aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
...
* Have the feedback bus as a backend for dumping globs.Gravatar Carst Tankink2014-04-10
|
* Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps ↵Gravatar Pierre Boutillier2014-04-09
| | | | | | | | | with -R. (Fix for Rocq/Rational.)" This reverts commit 7d3ce4012a53b123dac95381bf46aac65f865d69. Conflicts: CHANGES
* Add an option -Q (tentative name).Gravatar Guillaume Melquiond2014-04-08
| | | | | | 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.
* Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. ↵Gravatar Guillaume Melquiond2014-04-07
| | | | (Fix for Rocq/Rational.)
* Change handling of loadpath and mlpath.Gravatar Guillaume Melquiond2014-04-06
| | | | | | | | | | | | | - 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.
* STM: be more resilient to explicit Back + Sideff commands (closes: 3251)Gravatar Enrico Tassi2014-04-02
|
* Removing dead code in Tactics.Gravatar Pierre-Marie Pédrot2014-03-31
|
* Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Gravatar Pierre-Marie Pédrot2014-03-26
|
* STM: when an error occurs in a worker send back a bunch of statesGravatar Enrico Tassi2014-03-26
| | | | | | | | In this way when the user fixes the script only a small part of the broken proof has to be recomputed on master. The density of states sent back decreases as they get far from the error. I.e. counting from the error, the worker sends back states at distance 0 1 2 3 5 7 10 14 19 26 35 47...
* Adding a Print Strategy vernacular command. It allows to check theGravatar Pierre-Marie Pédrot2014-03-19
| | | | transparent status of variables and constants.
* STM: make the slave start from the most recent known stateGravatar Enrico Tassi2014-03-18
|
* STM: make -async-proofs on work from coqc tooGravatar Enrico Tassi2014-03-18
|
* fix compilation with ocaml < 4Gravatar Enrico Tassi2014-03-13
|
* STM: perspective (tell the scheduler what the user sees)Gravatar Enrico Tassi2014-03-13
|
* STM: move out a couple of submodulesGravatar Enrico Tassi2014-03-13
| | | | | These modules are not as reusable as one may want them to be, but moving them out simplifies a little STM.
* Stm: smarter delegation policyGravatar Enrico Tassi2014-03-12
| | | | | | | | | | | | | | | | | | | | Stm used to delegate every proof when it was possible, but this may be a bad idea. Small proofs may take less time than the overhead delegation implies (marshalling, etc...). Now it delegates only proofs that take >= 1 second. By default a proof takes 1 second (that may be wrong). If the file was compiled before, it reuses the data stored in the .aux file and assumes the timings are still valid. After a proof is checked, Coq knows how long it takes for real, so it wont predict it wrong again (when the user goes up and down in the file for example). CoqIDE now sends to Coq, as part of the init message, the file name so that Coq can load the .aux file.
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
| | | | | | | | | | | | | | | | | | Universes that are computed in the vi2vo step are not part of the outermost module stocked in the vo file. They are part of the Library.seg_univ segment and are hence added to the safe env when the vo file is loaded. The seg_univ has been augmented. It is now: - an array of universe constraints, one for each constant whose opaque body was computed in the vi2vo phase. This is useful only to print the constants (and its associated constraints). - a union of all the constraints that come from proofs generated in the vi2vo phase. This is morally the missing bits in the toplevel module body stocked in the vo file, and is there to ease the loading of a .vo file (obtained from a .vi file). - a boolean, false if the file is incomplete (.vi) and true if it is complete (.vo obtained via vi2vo).
* Using Hashmaps by default in constant and inductive maps. This changes fold andGravatar Pierre-Marie Pédrot2014-03-07
| | | | iter order, but it seems nobody was relying on it (contrarily to the string case).
* Lets coqtop use a slashGravatar Virgile Prevosto2014-03-06
|
* Using HMaps in Safe_env.environments, hopefully improving performances.Gravatar Pierre-Marie Pédrot2014-03-05
|
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
| | | | The removed code isn't used locally and isn't exported in the signature
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* STM: fix Show ScriptGravatar Enrico Tassi2014-03-04
|
* STM: when finish a task hcons universe constraintsGravatar Enrico Tassi2014-03-04
|
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
| | | | | | | There are currently two other clashs : Lexer and Errors, but for the moment these ones haven't impacted my experiments with extraction and compiler-libs, while this Matching issue had. And anyway the new name is more descriptive, in the spirit of the recent TacticMatching.
* Migrate back g_obligations in toplevelGravatar Pierre Letouzey2014-03-02
| | | | | | | | | | | | | | | | This almost reverts commit 845d6f (r15248). It isn't ideal to put syntactic stuff in the toplevel directory. Maybe this kind of files should have someday their own directory along with g_rewrite.ml4 and some other (maybe a extraparsing dir?). Meanwhile, this commit leads to a cleaner situation concerning *.ml4: - everything needed to build grammar.cma (and q_constr.cmo) is in: lib/ kernel/ library/ pretyping/ interp/ proofs/ parsing/ grammar/ - all *.ml4 using grammar.cma (or q_constr.cmo) are in: tactics/ toplevel/ plugins/*/
* Useless check when loading notations through import.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Removing a fishy use of pervasive equality in Ltac backtrace printing.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Gravatar Arnaud Spiwack2014-02-27
| | | | Impacts MapleMode.
* 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
|
* STM: better messages when checking/finishing tasksGravatar 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
|
* 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).
* Fixing printing of only_parsing notations.Gravatar Pierre-Marie Pédrot2014-02-25
|
* Simpl_behaviour becomes Reductionops.ReductionBehaviourGravatar Pierre Boutillier2014-02-24
| | | | syntax mentionning simpl remains
* Dead Code eliminationGravatar Pierre Boutillier2014-02-24
|
* Timeout and Set Default Timeout fixed (closes: #3229)Gravatar Enrico Tassi2014-02-10
|
* STM: when a worker is canceled mark the proof as brokenGravatar Enrico Tassi2014-02-10
|
* STM: be conservative w.r.t. proofs containing global side effectsGravatar Enrico Tassi2014-02-10
|
* Removing the [Require "file"] syntax.Gravatar Pierre-Marie Pédrot2014-02-02
|
* CUnix: enriched (get_extension, sys_command, waitpid_non_intr) + cleanedGravatar Pierre Letouzey2014-01-30
|
* Mltop: explicitly qualify calls to CUnixGravatar Pierre Letouzey2014-01-30
|
* Load implemented in CoqIDE/STM (closes: #3223)Gravatar Enrico Tassi2014-01-30
|
* STM + CoqIDE: stop_worker message and UIGravatar Enrico Tassi2014-01-30
|
* Work around for bug in threads + blocking io streamlinedGravatar Enrico Tassi2014-01-30
|
* STM: worker sends back to master the last valid stateGravatar Enrico Tassi2014-01-30
| | | | | So that the master process does not require to compute it. Still not all valid states are sent back.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 00:28:53 +0000