| Commit message (Collapse) | Author | Age |
|
|
|
| |
We also add a Coq86.v compat file.
|
|
|
|
|
|
| |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
|
|
|
| |
For Drop for example.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
|\ |
|
| | |
|
|\| |
|
| | |
|
|\| |
|
| |
| |
| |
| |
| |
| | |
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
| |
| |
| |
| |
| |
| | |
This patch should get rid of the following warning:
Invalid character '-' in identifier "v8-syntax".
|
|\| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
subdirectories.
Using Mltop.add_path instead of Mltop.add_rec_path causes the following
kind of behavior:
$ coqtop -nois
Coq < Require Import Coq.Init.Datatypes.
Error: Cannot find a physical path bound to logical path Coq.Init.
The only case where its use is still warranted is the implicit "." path. It
shall not be recursive because Coq might be called from about anywhere.
This patch also removes -I-as since its behavior is no longer the one from
8.4 so it is not worth keeping it around.
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
together with the tactic monad.
The move is not complete yet, because some file candidates for this directory
have almost useless dependencies in other ones that should not be moved.
|
| |
| |
| |
| | |
This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
|
|/ |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- The earlier proof-of-concept file NPeano (which instantiates
the "Numbers" framework for nat) becomes now the entry point
in the Arith lib, and gets renamed PeanoNat. It still provides
an inner module "Nat" which sums up everything about type nat
(functions, predicates and properties of them).
This inner module Nat is usable as soon as you Require Import Arith,
or just Arith_base, or simply PeanoNat.
- Definitions of operations over type nat are now grouped in a new
file Init/Nat.v. This file is meant to be used without "Import",
hence providing for instance Nat.add or Nat.sqrt as soon as coqtop
starts (but no proofs about them).
- The definitions that used to be in Init/Peano.v (pred, plus, minus, mult)
are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul
where here Nat is Init/Nat.v).
- This Coq.Init.Nat module (with only pure definitions) is Include'd
in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat
sometimes instead of just Nat (for instance when doing "Print plus").
Normally it should be ok to just ignore these "Init" since
Init.Nat is included in the full PeanoNat.Nat. I'm investigating if
it's possible to get rid of these "Init" prefixes.
- Concerning predicates, orders le and lt are still defined in Init/Peano.v,
with their notations "<=" and "<". Properties in PeanoNat.Nat directly
refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat
also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le",
we cannot yet include an Inductive to implement a Parameter), but these
aliased predicates won't probably be very convenient to use.
- Technical remark: I've split the previous property functor NProp in
two parts (NBasicProp and NExtraProp), it helps a lot for building
PeanoNat.Nat incrementally. Roughly speaking, we have the following schema:
Module Nat.
Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *)
... (** proofs of specifications for basic ops such as + * - *)
Include NBasicProp. (** generic properties of these basic ops *)
... (** proofs of specifications for advanced ops (pow sqrt log2...)
that may rely on proofs for + * - *)
Include NExtraProp. (** all remaining properties *)
End Nat.
- All other files in directory Arith are now taking advantage of PeanoNat :
they are now filled with compatibility notations (when earlier lemmas
have exact counterpart in the Nat module) or lemmas with one-line proofs
based on the Nat module. All hints for database "arith" remain declared
in these old-style file (such as Plus.v, Lt.v, etc). All the old-style
files are still Require'd (or not) by Arith.v, just as before.
- Compatibility should be almost complete. For instance in the stdlib,
the only adaptations were due to .ml code referring to some Coq constant
name such as Coq.Init.Peano.pred, which doesn't live well with the
new compatibility notations.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
lib/interface split into:
- lib/feedback
subscribe-based feedback bus (also used by coqidetop)
- ide/interface
definition of coqide protocol messages
lib/pp
structured info/err/warn messages
lib/serialize split into:
- lib/serialize
generic xml serialization (list, pairs, int, loc, ...)
used by coqide but potentially useful to other interfaces
- ide/xmlprotocol
serialization of protocol messages as in ide/interface
the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
|
|
|
|
|
|
|
|
|
|
|
|
| |
User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/
and pass -toploop footop to customize the coq main loop.
A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to
functions respectively initializing the toploop (and parsing toploop
specific arguments) and running the main loop itself.
For backward compatibility -ideslave and -async-proofs worker do
set the toploop to coqidetop and stmworkertop respectively.
|
|
|
|
|
|
| |
This option complements -I-as and -R. As the two other options, it adds a
new loadpath, but contrarily to them, files are not looked into the
directory unless fully qualified.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Option -I no longer handles loadpath, only mlpath. This is the same
behavior as coq_makefile. Option -I-as is unchanged.
- Option -R no longer recursively adds to mlpath; only the root directory
is added.
- user-contrib/ and xdg directories are no longer recursively added to
the loadpath.
- theories/ and plugins/ are no longer recursively added to the loadpath
when option -nois is passed.
- All the preconfigured directories are still recursively added to the
mlpath though.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Revised Coqtop.parse_args in a cleaner and lighter style
- Improved error message in case of argument parse failure:
* tell which option is expecting a related argument
* in case of unknown options, warn about them all at once
* do not hide the previous error messages by filling the
screen with usage(). Instead, suggest the use of --help.
- Specialized boolean config field Coq_config.arch_is_win32
- Faster Envars.coqlib, which is back to (unit->string), and
just access Flags.coqlib. Caveat: it must be initialized once
via Envars.set_coqlib
- Avoid keeping an opened channel to the "revision" file
- Direct load of theories/init/prelude.vo, no detour via Loadpath
Beware : ./configure must be runned after this commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Ok, this is merely a matter of taste, but up to now the usage
in Coq is rather to use capital letters instead of _ in the
names of inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
exception information addition facility.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16213 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
I hope I did not forget some [with] clauses. Otherwise, some
stack frame will be missing from the debug.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16167 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16161 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
This correspond to ocaml4 warning 6
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16053 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16005 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
compiler warnings).
I was afraid that such a brutal refactoring breaks some obscure
invariant about linking order and side-effects but the standard
library still compiles.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
For starting a bare coqtop, the recommended option is now "-noinit"
that skips the load of Prelude.vo. Option "-nois" is kept for
compatibility, it is now an alias to "-noinit".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Suppose we declare : Notation foo := bar (compat "8.3").
Then each time foo is used in a script :
- By default nothing particular happens (for the moment)
- But we could get a warning explaining that
"foo is bar since coq > 8.3".
For that, either use the command-line option -verb-compat-notations
or the interactive command "Set Verbose Compat Notations".
- There is also a strict mode, where foo is forbidden : the previous
warning is now an error.
For that, either use the command-line option -no-compat-notations
or the interactive command "Unset Compat Notations".
When Coq is launched in compatibility mode (via -compat 8.x),
using a notation tagged "8.x" will never trigger a warning or error.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Clib that does not depend on camlpX and is made to be shared by all coq
tools/scripts/...
- Lib that is Coqtop specific
As a side effect for the build system :
- Coq_config is in Clib and does not appears in makefiles
- only the BEST version of coqc and coqmktop is made
- ocamlbuild build system fails latter but is still broken
(ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14714 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
it is imcompatible with the freedesktop policy that config directory is private.
Feel absolutly free to revert this commit if you think -user should stay
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14713 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14696 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
From Tom Prince
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14692 85f007b7-540e-0410-9357-904b9bb8a0f7
|