| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
STM falls back to local, lazy, evaluation if the slave dies badly or
if there is a marshalling error. Both things should never occur, but
is nice to have the system recover if a bug pops up.
Nevertheless during regression testing these fallbacks should be
disabled not to hide a new bug.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16841 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16839 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- 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
|
|
Stm contains many TODO items to improve the thing, but it should
be already possible to play with it (but not use it in production).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16684 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16679 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Main changes for STM:
1) protocol changed to carry edit/state ids
2) colouring reflects the actual status of every span (evaluated or not)
3) button to force the evaluation of the whole buffer
4) cmd_stack and backtracking completely changed to use state numbers
instead of counting sentences
5) feedback messages are completely asynchronous, and the whole protocol
could be made so with a minor effort, but there is little point in it
right now. Left as a future improvement. Missing bit: add
sentence-id to responses of interp command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The process_transaction function adds a new edge to the Dag without
executing the transaction (when possible).
The observe id function runs the transactions necessary to reach to the
state id. Transaction being on a merged branch are not executed but
stored into a future.
The finish function calls observe on the tip of the current branch.
Imperative modifications to the environment made by some tactics are
now explicitly declared by the tactic and modeled as let-in/beta-redexes
at the root of the proof term. An example is the abstract tactic.
This is the work described in the Coq Workshop 2012 paper.
Coq is compile with thread support from now on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
parametric on the list of possible flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16665 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16555 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16537 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
full usage of notations instead of the previous cheap way to prevent
circularity in printing by deactivating all notations.
(Since "->" became a notation, printing abbreviations without
notations at all had become even more inconvenient).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16470 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16454 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16442 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This commit introduces 2 new vernac_expr constructors:
- VernacLocal (b,v) that represents a vernacular v with the "Local" modifier
- VernacProgram v that represents a vernacular v with the "Program" modifier
This allows the parser to avoid using side effects to model the two
modifiers, that are now represented in the AST. This also decouples the
parsing phase from the interpretation phase, since parsing a second
phrase does not alter the locality flag for the first phrase.
As a consequence all the locality_flag components of vernac_expr have
been removed, but for the ones that (for retro compatibility) allow
an "infix" Local flag. In these cases the boolean is renamed
obsolete_locality (as the grammar entry that parses it), and during
interpretation we check that at most one locality flag is specified,
using the idiom (where the input local is the obsolete one):
let local = enforce_XXX_locality locality local in
Another improvement is that the default locality is not chosen in the
parser, but in the interpreter where the idiom
let local = make_XXX_locality locality in
is used to default the locality to XXX (module/section/whatever).
Unfortunately not all side effects have been removed:
- Flags.program_mode is still used to signal that we are in program mode
- Locality.LocalityFixme.* functions are used in commands that do not
have an AST, but are parsed as VernacExtend (see vernacinterp.ml)
I guess one could fix the latter case systematically adding an extra
argument "locality" to commands attached using VERNAC COMMAND EXTEND.
Fixing plugins adding commands that honour "Local" should look like this:
VERNAC COMMAND EXTEND Set_Solver
| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
set_default_tactic
- (Locality.use_section_locality ())
+ (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
(Tacintern.glob_tactic t) ]
END
In any case the side effects are set/consumed within then interpretation
phase, and not set during the parsing phase and consumed during the
interpretation phase.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16396 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
compiler (implemented on Matthieu's request).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16240 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
|
|
native OCaml code.
Warning: the "retroknowledge" mechanism has not been ported to the native
compiler, because integers and persistent arrays will ultimately be defined as
primitive constructions. Until then, computation on numbers may be faster using
the VM, since it takes advantage of machine integers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15970 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
writing our own comparison functions, and enforcing monomorphization
in many places. This should be more efficient, btw. Still a work
in progress.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 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
|
|
This bling-bling feature is interacting badly with
- the documentation generation
- the bench logs
- compilation in an emacs buffer
- ...
As long as these points aren't solved, no coloring by default,
but on the contrary an option to manually activate it: coqtop -color
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15427 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15421 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15247 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Remove useless functorization of Pretyping
- Move Program coercion/cases code inside pretyping/, enabled according
to a flag.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
I assume that once Coq is installed in non-local mode and run from its
installed path, sources are no longer available. The coqsrc variable
doesn't make any sense, then, and its intended value can always be
inferred from Sys.executable_name. Moving it to Envars.coqroot.
Make coqlib optional. Currently, it is set to None only in -local mode
or with ocamlbuild. When set to None, -local layout is assumed
(binaries in ./bin, library in .). The behaviour should not be changed
when an explicit coqlib has been given to ./configure.
This commit should make it possible to run a Coq compiled with -local
from anywhere (no hard-coded absolute path embedded in the
executables, intermediary step to bug #2565). It WILL BREAK settings
re-using source trees after installation in non-local mode (are there
actual use cases for that?).
Hard-coded absolute paths still remain:
- in the build system, so the need to re-run ./configure after moving
the source tree is still expected for now;
- in coqrunbyteflags, I think we are limited by ocaml itself;
- docdir.
All absolute paths should be removed, ultimately.
As a side-effect, simplify computing of Envars.coqbin. I don't see any
good reason to keep it as a function.
Disclaimers:
- initialization of Sys.executable_name is not consistent across all
architectures; relying so much on it might trigger bugs. I'm pretty
sure something will explode if one adds arbitrary symlinks on top of
that;
- ocamlbuild stuff not tested.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
when printing.
Signed-off-by: Tom Prince <tom.prince@ualberta.net>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14284 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
use_pattern_unification common for evars and metas. As a compensation,
add a flag use_meta_bound_pattern_unification to restore the old
mechanism of pattern unification for metas applied to rels only (this
is used e.g. by auto). Not sure yet, what could be the most
appropriate set of flags. Added documentation of the flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14221 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
inserting special chars for proof by pointing with emacs. This was
interacting badly with utf8. It may be implemented back with xml-like
tags instead of special chars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14154 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The recent experiment with -dont-load-proofs in the stdlib showed that
this options isn't fully safe: some axioms were generated (Include ?
functor application ? This is still to be fully understood).
Instead, I've implemented an idea of Yann: only load opaque proofs when
we need them. This is almost as fast as -dont-load-proofs (on the stdlib,
we're now 15% faster than before instead of 20% faster with -dont-load-proofs),
but fully compatible with Coq standard behavior.
Technically, the const_body field of Declarations.constant_body now regroup
const_body + const_opaque + const_inline in a ternary type. It is now either:
- Undef : an axiom or parameter, with an inline info
- Def : a transparent definition, with a constr_substituted
- OpaqueDef : an opaque definition, with a lazy constr_substitued
Accessing the lazy constr of an OpaqueDef might trigger the read on disk of
the final section of a .vo, where opaque proofs are located.
Some functions (body_of_constant, is_opaque, constant_has_body) emulate
the behavior of the old fields. The rest of Coq (including the checker)
has been adapted accordingly, either via direct access to the new const_body
or via these new functions. Many places look nicer now (ok, subjective notion).
There are now three options: -lazy-load-proofs (default), -force-load-proofs
(earlier semantics), -dont-load-proofs. Note that -outputstate now implies
-force-load-proofs (otherwise the marshaling fails on some delayed lazy).
On the way, I fixed what looked like a bug : a module type
(T with Definition x := c) was accepted even when x in T was opaque.
I also tried to clarify Subtyping.check_constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
As said in CHANGES:
<<
The inlining done during application of functors can now be controlled
more precisely. In addition to the "!F G" syntax preventing any inlining,
we can now use a priority level to select parameters to inline :
"<30>F G" means "only inline in F the parameters whose levels are <= 30".
The level of a parameter can be fixed by "Parameter Inline(30) foo".
When levels aren't given, the default value is 100. One can also use
the flag "Set Inline Level ..." to set a level.
>>
Nota : the syntax "Parameter Inline(30) foo" is equivalent to
"Set Inline Level 30. Parameter Inline foo.",
and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G."
For instance, in ZBinary, eq is @Logic.eq and should rather be inlined,
while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined.
We could achieve this behavior by setting a level such as 30 to the
parameter eq, and then tweaking the current level when applying functors.
This idea of levels might be too restrictive, we'll see, but at least
the implementation of this change was quite simple. There might be
situation where parameters cannot be linearly ordered according to their
"inlinablility". For these cases, we would need to mention names to inline
or not at a functor application, and this is a bit more tricky
(and might be a pain to use if there are many names).
No documentation for the moment, since this feature is experimental
and might still evolve.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
According to B. Gregoire, this stuff is obsolete. Fine control
on when to launch the VM in conversion problems is now provided
by VMcast. We were already almost never boxing definitions anymore
in stdlib files.
"(Un)Boxed Definition foo" will now trigger a parsing error,
same with Fixpoint. The option "(Un)Set Boxed Definitions"
aren't there anymore, but tolerated (as no-ops), since unknown
options raise a warning instead of an error by default.
Some more cleaning could be done in the vm.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
coqide doc link is the canonical link to last released version of
reference manual instead of link to corresponding coqide version).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13436 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13389 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
proofs is now the default behavior of coqtop.
* lib/Coqtop: Update accordingly.
* checker/Check library/Library:
Pass the right "load_proofs" flag to LightenLibrary.load.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13379 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
requiring a file Utf8_core. That needs to be improved...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13358 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
people use the undocumented "Lemma foo x : t" feature in a way
incompatible with this activation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Fixed some bugs in -beautify and robustness of {struct} clause.
Note: I tried to make the Automatic Introduction mode on by default
for version >= 8.3 but it is to complicated to adapt even in the
standard library.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12546 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Compatibility version is now a global parameter that every feature can
individually browse. This avoids having to keep the names of options
synchronous in their respective files and in now-removed file coqcompat.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12372 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
colon in (mutual) proofs with [Set Automatic Introduction].
Fix a minor test-suite issue in ProgramWf due to new handling of the
default obligation tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12351 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In trunk: New strategy for compiling and finding index_url.txt. After
all, this file is not specific to CoqIDE but to the
documentation. Hence, it seems better to install it close to the
documentation. If the documentation is locally installed, it is easy
to find the file index_url.txt but what to do if the documentation is
remote? We would need a http getter. Does this mean we have to rely on
wget or so? In the absence of answer to this question, it seems
reasonable, first to assume the doc to be locally installed, second to
have a local copy of index_url.txt ready in the installation directory
of CoqIDE.
Also added an "automatic" field in the CoqIDE url preference to
prevent the user to have to update his preference file every time a
new version of Coq is out and the link to the doc change.
In 8.2: Added a minima the installation of index_urls.txt but the user
will have to update its preferences because the links
"http://coq.inria.fr/doc/Reference-Manual010.html#..." do not longer
exist.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12278 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Filtering of doc compilation messages (11793,11795,11796).
- Fixing bug #1925 and cleaning around bug #1894 (11796, 11801).
- Adding some tests.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
principaux changements sont:
- coqtop (et coqc) maintenant insensible aux variables
d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les
librairies Coq peut être spécifié par l'option -coqlib
- coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et
-camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les
chemins des exécutables OCaml; en dehors du mode boot, coqmktop
cherche les exécutables OCaml dans PATH
- installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci
étant installé en copiant l'architecture des sources (ie lib.cmxa
est installé dans COQLIB/lib/lib.cmxa)
- coq_makefile prend maintenant 3 paramètres sous forme de variables
d'environnement: COQBIN pour dire où trouver les exécutables Coq,
CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les
chemins vers les librairies sont déduits en utilisant -where
Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de
simuler les conditions de la vie réelle (Ocaml pas dans le PATH,
installation binaire relocalisée, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
|
