aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
| | | | | NB: new file miscprint.ml deserves to be part of printing.cma, but should be part of proofs.cma for the moment, due to use in logic.ml
* Removing generic equality in Syntax plugin.Gravatar Pierre-Marie Pédrot2014-03-02
|
* Adding an equality function over glob_constrGravatar Pierre-Marie Pédrot2014-03-02
|
* Fixing generic Hashtbl.hash in Constr.Gravatar Pierre-Marie Pédrot2014-03-02
|
* Fix syntax highlighting of "Implicit Arguments" for gtksourceview.Gravatar Guillaume Melquiond2014-03-02
|
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
|
* Better behaviour for sets of reserved names.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Never suppress the typing constraint of bound variables whose name wasGravatar Pierre-Marie Pédrot2014-03-01
| | | | reserved with Implicit Type.
* Fixing bad comparison in Detyping.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Useless check when loading notations through import.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Hunting pervasive equality in native compiler. It seems they were used forGravatar Pierre-Marie Pédrot2014-03-01
| | | | | optimization purposes. I replaced their use with the under-approximation of pointer equality.
* Removing a fishy use of pervasive equality in Ltac backtrace printing.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Removing Pervasives.compare in Termdn.Gravatar Pierre-Marie Pédrot2014-02-28
|
* Removing a Pervasives.compare in Term_dnet.Gravatar Pierre-Marie Pédrot2014-02-28
|
* Pos.compare_cont takes the comparison as first argumentGravatar Pierre Boutillier2014-02-28
| | | | Helps cbn tactic refolding
* Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an ↵Gravatar Pierre Boutillier2014-02-28
| | | | infinite loop.
* test-suite: opaque term -> opaque proofGravatar Pierre Boutillier2014-02-28
|
* test-suite: New names for vars but the expected invariant is preservedGravatar Pierre Boutillier2014-02-28
|
* Fix output test-suite 'simpl tactic' -> 'reduction tactics'Gravatar Pierre Boutillier2014-02-28
|
* Dead code elimionation in reductionopsGravatar Pierre Boutillier2014-02-28
|
* .*.aux erased by make distcleanGravatar Pierre Boutillier2014-02-28
|
* Fix compilation of coq and plugins using coq_makefile under cygwinGravatar Enrico Tassi2014-02-28
| | | | | | | | | Problems: - strip may not be "strip" but "i686-bla-strip", hence we ask ocamlc -config the value of "ranlinb" and replace ranlib by strip obtaining "i686-bla-strip" from "i686-bla-ranlib" - coq_makefile was not quoting the plugins/ paths - coq_makefile was quoting twice camlpX (the shell of cygwin was confused)
* Fixing a Pervasive.compare.Gravatar Pierre-Marie Pédrot2014-02-28
|
* Makefile: re-introduce 2 phases to avoid make strange -include'sGravatar Pierre Letouzey2014-02-27
| | | | | | | | | | | | | | | | | | | | | | | | | Yet another revision of the build system. We avoid relying on the awkward include-which-fails-but-works-finally-after-a-retry feature of gnu make. This was working, but was quite hard to understand. Instead, we reuse the idea of two explicit phases (as in 2007 and its stage{1,2,3}), but in a lighter way. The main Makefile calls Makefile.build twice : - first for building grammar.cma (and q_constr.cmo), with a restricted set of .ml4 to consider (see variables BUILDGRAMMAR and ML4BASEFILES). - then on the true target(s) asked by the user (using the special variable MAKECMDGOALS). In pratice, this should change very little to the concrete developper's life, let me know otherwise. A few more messages of make due to the explicit first sub-call, but no more strange "not ready yet" messages... Btw: we should handle correctly now the parallel compilation of multiple targets (e.g. make -jX foo bar). As reported by Pierre B, this was triggering earlier two separate sub-calls to Makefile.build, one for foo, the other for bar, with possibly nasty interactions in case of parallelism. In addition, some cleanup of Makefile.build, removal of useless :: rules, etc etc.
* amending last commitGravatar Enrico Tassi2014-02-27
|
* better warningGravatar Enrico Tassi2014-02-27
|
* Tacinterp: more refactoring.Gravatar Arnaud Spiwack2014-02-27
| | | Introducing List.fold_right and List.fold_left in Monad.
* Tacinterp: refactoring using Monad.Gravatar Arnaud Spiwack2014-02-27
| | | Adds a combinator List.map_right which chains effects from right to left.
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
|
* Remove unsafe code (Obj.magic) in Tacinterp.Gravatar Arnaud Spiwack2014-02-27
| | | This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
* Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Gravatar Arnaud Spiwack2014-02-27
| | | | Impacts MapleMode.
* Get rid of the enterl/glist API for Proofview.Goal.Gravatar Arnaud Spiwack2014-02-27
| | | The prefered style is to use continuation passing style when necessary, or simply passing the goal explicitely in the case of interpretation functions which do not evolve the current goal.
* Tacinterp: yet another superfluous enterl.Gravatar Arnaud Spiwack2014-02-27
|
* Tacinterp: spurious enterl.Gravatar Arnaud Spiwack2014-02-27
| | | This changes the tacinterp API, but only affects (one line of) the MapleMode contrib.
* Dead code: eval_ltac_constr.Gravatar Arnaud Spiwack2014-02-27
|
* STM: better debug messagesGravatar Enrico Tassi2014-02-26
|
* STM: do not print goals on UndoGravatar Enrico Tassi2014-02-26
|
* CoqIDE: print message of "Fail" commandGravatar Enrico Tassi2014-02-26
|
* refman: document vi2voGravatar Enrico Tassi2014-02-26
|
* STM: better messages when checking/finishing tasksGravatar Enrico Tassi2014-02-26
|
* Library: when compiling multiple files, reset the opaque tablesGravatar Enrico Tassi2014-02-26
| | | | | That was a bug. coqc a b was generating (for b) an opaque table containing also the proofs of a.
* STM: when batch compiling a vo, assert we behave conservativelyGravatar Enrico Tassi2014-02-26
| | | | | This meas that the list of future_constraints in safe_env is empty, meaning that nothing was delayed.
* coq_makefile: new target vi2voGravatar Enrico Tassi2014-02-26
|
* vi2vo: new flag -schedule-vi2voGravatar Enrico Tassi2014-02-26
|
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
| | | | | Make this module deal only with opaque proofs. Make discharging/substitution invariant more explicit via a third constructor.
* STM: backup/restore remote countersGravatar Enrico Tassi2014-02-26
|
* remoteCounter: backup/restoreGravatar Enrico Tassi2014-02-26
| | | | | When you resume the compilation of a .vi file, you want to avoid collisions on fresh names.
* univ: removing dead codeGravatar Enrico Tassi2014-02-26
|
* checker and votour ported to new vo format (after -vi2vo)Gravatar Enrico Tassi2014-02-26
|
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 07:30:07 +0000