| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
| |
|
|
| |
lib/cErrors.ml)
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When an axiom of an empty type is matched in order to inhabit
a type, do print that type (as if each use of that axiom was a
distinct foo_subproof).
E.g.
Lemma w : True.
Proof. case demon. Qed.
Lemma x y : y = 0 /\ True /\ forall w, w = y.
Proof. split. case demon. split; [ exact w | case demon ]. Qed.
Print Assumptions x.
Prints:
Axioms:
demon : False
used in x to prove: forall w : nat, w = y
used in w to prove: True
used in x to prove: y = 0
|
| |
|
|
|
|
| |
Although these commands were never deprecated, they have been unusable for some
time now, since they send requests to an Italian server which is no longer
alive.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
files around. A bunch of files from lib/ that were only used in the STM were
moved, as well as part of toplevel/ related to the STM.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
To obtain a.vo one can now:
1) coqtop -quick -compile a
2) coqtop -vi2vo a.vi
To make that possible the .vo structure has been complicated. It is now
made of 5 segments.
| vo | vi | vi2vo | contents
--------------+------+-----+-------+------------------------------------
lib | Yes | Yes | Yes | libstack (modules, notations,...)
opauqe_univs | No | Yes | Yes | constraints coming from opaque proofs
discharge | No | Yes | No | data needed to close sections
tasks | No | Yes | No | STM tasks to produce proof terms
opaque_proofs | Yes | Yes | Yes | proof terms
--------------+------+-----+-------+------------------------------------
This means one can load only the strictly necessay parts. Usually one
does not load the tasks segment of a .vi nor the opaque_proof segment of
a .vo, unless one is turning a .vi into a .vo, in which case he load
all the segments.
Optional segments are marshalled as None. But for lib, all segments
are Array.t of:
| type
--------------+---------------------------------------------------------
lib | a list of Libobject.obj (n'importe quoi)
opauqe_univs | Univ.consraints Future.computation
discharge | what Cooking.cook_constr needs
tasks | Stm.tasks (a task is system_state * vernacexpr list)
opaque_proofs | Term.constr Future.computation
--------------+------+-----+-------+------------------------------------
Invariant: all Future.computation in a vo file (obtained by a vi2vo
compilation or not) have been terminated with Future.join (or
Future.sink). This means they are values (inside a box).
This invariant does not hold for vi files. E.g. opauqe_proofs can be
dangling Future.computation (i.e. NotHere exception). The vi2vo
compilation step will replace them by true values.
Rationale for opaque_univs: in the vi2vo transformation we want to reuse
the lib segment. Hence the missing pieces have to be put on the side,
not inside. Opaque proof terms are already in a separte segment.
Universe constraints are not, hence the new opauqe_univs segment. Such
segment, if present in a .vo file, is always loaded, and
Declare.open_constant will add to the environment the constraints stored
there. For regular constants this is not necessay since the constraints
are already in their enclosing module (and also in the constant_body).
With vi2vo the constraints coming from the proof are not in the
constant_body (hence not in the enclosing module) but there and are
added to the environment explicitly by Declare.open_constant.
Rationale for discharge: vi2vo produces a proof term in its original
context (in the middle of a section). Then it has to discharge the
object. This segment contains the data that is needed in order to do
so. It is morally the input that Lib.close_section passes to Cooking
(via the insane rewinding of libstack, GlobalRecipe, etc chain).
Checksums: the checksum of .vi and a .vo obtain from it is the same.
This means that if if b.vo has been compiled using a.vi, and then
a.vi is compiled into a.vo, Require Import b works (and recursively
loads a.vo).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The command `coqtop -check-vi-tasks 1,4,2 a` checks tasks 1 4 2,
in this precise order, stored in a.vi.
The command `coqtop -schedule-vi-checking 4 a b c` reads {a,b,c}.vi
and .{a,b,c}.aux and spits 4 command lines to check all the tasks in
{a,b,c}.vi trying to equally partition the job between the 4 workers,
that can indeed be run in parallel.
The aux file contains the time that it took to check the proofs stored
in the .vi files last time the file was fully checked.
This user interface is still very rough, it should probably run the
workers instead of just printing their command line.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
* vars.mli was mentionning Term instead of Constr, leading to a dep cycle
* Having a file named toplevel/toplevel.ml isn't a good idea when we also
have a toplevel/toplevel.mllib that ought to produce a toplevel.cma.
We rename toplevel.ml into Coqloop.ml
* Extra cleanup of toplevel.mllib :
- Ppextra isn't anywhere around (?!)
- Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway
- Vernacexpr is a .mli and shouldn't appear in an .mllib
* During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml)
* A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread
for coqchk).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The warning output by vernacextend when the classifier is missing
is the documentation of this commit:
Warning: Vernac entry "Foo" misses a classifier. A classifier is a
function that returns an expression of type vernac_classification (see
Vernacexpr). You can:
- Use '... EXTEND Foo CLASSIFIED AS QUERY ...' if the new
vernacular command does not alter the system state;
- Use '... EXTEND Foo CLASSIFIED AS SIDEFF ...' if the new
vernacular command alters the system state but not the parser nor it starts
a proof or ends one;
- Use '... EXTEND Foo CLASSIFIED BY f ...' to specify a global
function f. The function f will be called passing "Foo" as the
only argument;
- Add a specific classifier in each clause using the syntax:
'[...] => [ f ] -> [...]'.
Specific classifiers have precedence over global classifiers. Only one
classifier is called.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16680 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
|
| |
|
|
|
|
|
|
|
|
|
|
| |
through a unique generic argument, and the level is only considered
at parsing time.
This may introduce unnecessary parentheses in Ltac printing though,
as every tactic argument is collapsed at the lowest level. I assume
this does not matter that much, and anyway Ltac printing is quite
bugged as of today.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16616 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
mechanism with the SearchAbout one. Searches may be slower, but this
is unlikely to be noticed. In addition, according to Hugo, the
Libtype summary was imposing a noticeable time penalty without
any real advantage.
Now Search and SearchPattern are the same. The documentation was not
really clear about the difference between both, except that Search
was restricted to closed terms. This is an artificial restriction by
now.
Fixing #2815 btw.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16320 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
Adds a directory ./intf for pure interfaces.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15248 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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Migrate the backtracking code from ide_slave.ml into a new backtrack.ml.
In particular the history stack of commands that used to be there is now
non-coqide-specific.
** Adapted commands **
- "Show Script": a basic functional version is restored (and the printing
of scripts at Qed in coqtop). No indentation, one Coq command per line,
based on the vernac_expr asts recorded in the history stack, printed via
Ppvernac.
- "Back n" : now mimics the backtrack of coqide: it goes n steps back
(both commands and proofs), and maybe more if needed to avoid re-entering
a proof (it outputs a warning in this case).
- "BackTo n" : still try to go back to state n, but it also handles the
proof state, and it may end on some state n' <= n if needed to avoid
re-entering a proof. Ideally, it could someday be used by ProofGeneral
instead of the complex Backtrack command.
** Compatible commands **
- "Backtrack" is left intact from compatibility with current ProofGeneral.
We simply re-synchronize the command history stack after each Backtrack.
- "Undo" is kept as a standard command, not a backtracking one, a bit like
"Focus". Same for "Restart" and "Abort". All of these are now accepted
in coqide (Undo simply triggers a warning).
- Undocumented command "Undo To n" (counting from start of proof instead of
from end) also keep its semantics, it is simply made compatible with
the new stack mechanism.
** New restrictions **
We now forbid backtracking commands (Reset* / Back*) inside files
when Load'ing or compiling, or inside VernacList/VernacTime/VernacFail.
Too much work dealing with these situation that nobody uses.
** Internal details **
Internally, the command stack differs a bit from what was in Ide_slave
earlier (which was inspired by lisp code in ProofGeneral). We now tag
commands that are unreachable by a backtrack, due to some proof being
finished, aborted, restarted, or partly Undo'ed. This induce a bit of
bookkeeping during Qed/Abort/Restart/Undo, but then the backtracking code
is straightforward: we simply search backward the first reachable state
starting from the desired place. We don't depend anymore on the proof
names (apart in the last proof block), It's more robust this way
(think of re-entering a M.foo from an outside proof foo).
Many internal clarifications in Lib, Vernac, etc. For instance
"Reset Initial" is now just a BackTo 1, while "Reset foo" now calls
(Lib.label_before_name "foo"), and performs a BackTo to the corresponding
label.
Concerning Coqide, we directly suppress the regular printing of goals
via a flag in Vernacentries. This avoid relying on a classification
of commands in Ide_slave as earlier.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15085 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
add_definition/fixpoint and parsing of the "Program" prefix.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
toplevel/
The code is not called yet from there.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15035 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
.mllib should only mention *code* to be linked in .cma
and later executable, but not .mli without .ml.
Otherwise, really nasty errors occur with ocamlbuild,
for instance some rules appears to be ignored and masked
by default ones, etc etc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14840 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
associated types (interface.mli), and an applicative part processing the calls (previous ide_intf).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14730 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14723 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14632 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Former module Ide_blob is now divided in Ide_intf (linked both
by coqtop and coqide) and Ide_slave (now only in coqtop).
Ide_intf has almost no dependencies, we can now compile coqide
with only coq_config.cm* and lib.cm(x)a
TODO:
- Devise a better way to display whether coqide is byte or opt
in the about message (instead of Mltop.is_native, I display
now the executable name, which hopefully contains opt or byte)
- Check the late error handling in ide/coq.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13927 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
Still messy.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
Interface
the ProtectedLoop feature was used only by CoqInterface.
Idem for stuff in Line_oriented_parser
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12573 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Cleaning and uniformisation in command.ml:
- For better modularity and better visibility, two files got isolated
out of command.ml:
- lemmas.ml is about starting and saving a proof
- indschemes.ml is about declaring inductive schemes
- Decomposition of the functions of command.ml into a functional part
and the imperative part
- Inductive schemes:
- New architecture in ind_tables.ml for registering scheme builders,
and for sharing and generating on demand inductive schemes
- Adding new automatically generated equality schemes (file eqschemes.ml)
- "_congr" for equality types (completing here commit 12273)
- "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep",
"_rew_backward" (similar to eq_rect), "_rew_backward_dep" for
rewriting schemes (warning, rew_forward_dep cannot be stated following
the standard Coq pattern for inductive types: "t=u" cannot be the
last argument of the scheme)
- "_case", "_case_nodep", "_case_dep" for case analysis schemes
- Preliminary step towards discriminate and injection working on any
equality-like type (e.g. eq_true)
- Restating JMeq_congr under the canonical form of congruence schemes
- Renamed "Set Equality Scheme" into "Set Equality Schemes"
- Added "Set Rewriting Schemes", "Set Case Analysis Schemes"
- Activation of the automatic generation of boolean equality lemmas
- Partial debug and error messages improvements for the generation of
boolean equality and decidable equality
- Added schemes for making dependent rewrite working (unfortunately with
not a fully satisfactory design - see file eqschemes.ml)
- Some names of ML function made more regular (see dev/doc/changes.txt)
- Incidentally, added a flush to obsolete Local/Global syntax warning
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
branch
and remove equations stuff which moves to a separate plugin.
Classes:
- Ability to define classes post-hoc from constants or inductive types.
- Correctly rebuild the hint database associated to local hypotheses when
they are changed by a [Hint Extern] in typeclass resolution.
Tactics and proofs:
- Change [revert] so that it keeps let-ins (but not [generalize]).
- Various improvements to the [generalize_eqs] tactic to make it more robust
and produce the smallest proof terms possible.
Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with
[generalize_eqs].
- A few new general purpose tactics in Program.Tactics like [revert_until]
- Make transitive closure well-foundedness proofs transparent.
- More uniform testing for metas/evars in pretyping/unification.ml
(might introduce a few changes in the contribs).
Program:
- Better sorting of dependencies in obligations.
- Ability to start a Program definition from just a type and no obligations,
automatically adding an obligation for this type.
- In compilation of Program's well-founded definitions, make the functional a
separate definition for easier reasoning.
- Add a hint database for every Program populated by [Hint Unfold]s for
every defined obligation constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- add coqtop option "-compat X.Y" so as to provide compatibility with
previous versions of Coq (of course, this requires to take care of
providing flags for controlling changes of behaviors!),
- add support for option names made of an arbitrary length of words
(instead of one, two or three words only),
- add options for recovering 8.2 behavior for discriminate, tauto,
evar unification ("Set Tactic Evars Pattern Unification", "Set
Discriminate Introduction", "Set Intuition Iff Unfolding").
Update of .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
* generalize the use of .mllib to build all cma, not only in plugins/
* the .mllib in plugins/ now mention Bruno's new _mod.ml files
* lots of .cmo enumerations in Makefile.common are removed, since
they are now in .mllib
* the list of .cmo/.cmi can be retreive via a shell script line,
see for instance rule install-library
* Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
_files_
* a -I option to coqdep_boot allows to control piority of includes
(some files with the same names in kernel and checker ...)
This is quite a lot of changes, you know who to blame / report to
if something breaks.
... and last but not least I've started playing with ocamlbuild.
The myocamlbuild.ml is far from complete now, but it already allows
to build coqtop.{opt,byte} here. See comments at the top of
myocamlbuild.ml, and don't hesitate to contribute, either for completing
or simplifying it !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Emilio Jesus Gallego Arias
Pierre Letouzey
Enrico Tassi
Maxime Dénès
Pierre-Marie Pédrot
gareuselesinge
ppedrot
letouzey
pboutill
msozeau
vgross
herbelin