aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
...
* RichPp: New module.Gravatar Regis-Gianas2014-11-04
| | | | | | | | | It is responsible for turning a tagged pretty-printing into a semi-structured document. clib.mllib: Include RichPp as well as Xml_*. The migration of Xml_* from lib to clib is needed by RichPp depends on these modules.
* Xml_datatype.gxml: New type for semi-structured documents.Gravatar Regis-Gianas2014-11-04
| | | | Xml_parser, Xml_printer: Use it.
* lib/Pp: Publish combinators for tags opening and closing.Gravatar Regis-Gianas2014-11-04
|
* lib/Pp.ppcmd_token:Gravatar Regis-Gianas2014-11-04
| | | | | | | Extend this type with Ppcmd_open_tag and Ppcmd_close_tag. lib/Pp.ppcmd_pp_dirs: Handle these tags with a straightforward translation to corresponding Format commands.
* lib/Pp: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* Add an [Info Level] option to print info traces automatically.Gravatar Arnaud Spiwack2014-11-01
| | | | [Set Info Level n] prints all info traces at level [n]. [Unset Info Level] stops the automatic printing of info traces. The unfolding level [n] can be overloaded by local [Info m tac] calls.
* Feedback message: hold extra info to help routingGravatar Enrico Tassi2014-10-31
| | | | | PIDE based GUIs can take advantage of multiple panels and get some feedback routed there. E.g. query panel
* STM: new worker for queriesGravatar Enrico Tassi2014-10-31
| | | | | | | | | | | | | | | | | | | | | | | | With the options -async-queries-always-delegate queries are always delegated to a worker process (Eval, Check, ...). Users of PIDE based UIs (in Denmark) reported that the current behavior of processing query synchronously is rather unexpected when one is used to get proofs processed asynchronously. Non instantaneous queries are part of many scripts and are there as "tests" for testing the execution of recursive functions. A standard proof script shape in an ongoing work by Appel and Bengtson is made of blocks like: - recursive function definition, - some tests, - some proofs And one cannot quickly jump over the tests (only the proofs). Enclosing the queries into dummy proofs to recover a reactive UI is just annoying. Hence this patch. Currently CoqIDE is not able to integrate the asynchronous feedback of the query workers into the document, hence if one passes the option to CoqIDE one only gets a boolean out of queries (processed/error).
* Changed implementation of lib/heap.ml to use Braun treesGravatar Jean-Christophe Filliatre2014-10-25
| | | | | | | | The previous implementation was embarrassingly naive and inefficient. For elements with the same priority, this new implementation may return a maximum element that is different (yet still with the highest priority, of course). This code is used only in tactic firstorder.
* -help failing (fix 3762)Gravatar Enrico Tassi2014-10-24
|
* Monad: change the error managing of two-list combinators.Gravatar Arnaud Spiwack2014-10-23
| | | Otherwise I risked catching errors from the argument functions when I wanted to catch size mismatch to add information to errors.
* Goal printing made uniform: always done in STM (close 3585)Gravatar Enrico Tassi2014-10-22
| | | | | | | | | | Goal printing was partially broken. Some commands in vernacentries were printing, but not all of them. Moreover an unlucky combination of `Flags.verbosely (fun () -> interp "Set Silent")` was making the silent flag not settable anymore. Now STM always print the open goals after a command when run in interactive mode via coqtop or emacs. More modern GUI do ask for the goals.
* An additional [List.iter] monadic combinator.Gravatar Arnaud Spiwack2014-10-22
|
* Add more primitives to the [Monad.Make] arguments.Gravatar Arnaud Spiwack2014-10-22
| | | | For optimisation purposes.
* Proofview: move [list_goto] to the [CList] module.Gravatar Arnaud Spiwack2014-10-22
| | | | It is, after all, a generic function about lists.
* Add a two-list monadic fold_left iterator.Gravatar Arnaud Spiwack2014-10-22
|
* Small optimisation in the monadic list combinators.Gravatar Arnaud Spiwack2014-10-22
| | | | The monadic bind can be costly, so sparing a few can be worth it. Therefore I unrolled the last element of the recursions. I took the opportunity to do some loop unrolling, which is probably more useful for map combinators than for fold.
* Factor module signatures.Gravatar Arnaud Spiwack2014-10-22
|
* When loading libraries, feed back dependencies.Gravatar Carst Tankink2014-10-13
| | | | | | | | These dependencies between files can be used by UIs to guide compilation and reloading of files. FileDependency (Some "/foo.v", "/bar.v") means foo depends on bar. FileDependency (None, "/bar.v") means the current file depends on bar.
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
|
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
| | | | | | | | | | | | | | Before this patch opaque tables were only growing, making them unusable in interactive mode (leak on Undo). With this patch the opaque tables are functional and part of the env. I.e. a constant_body can point to the proof term in 2 ways: 1) directly (before the constant is discharged) 2) indirectly, via an int, that is mapped by the opaque table to the proof term. This is now consistent in batch/interactive mode This is step 0 to make an interactive coqtop able to dump a .vo/.vi
* Fixup leading ./ path cleaningGravatar Pierre Boutillier2014-10-09
|
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
| | | | | | being able to export hints without tactics, vm, etc. to come with. Some functions moved to the new proof engine.
* A few improvements on pattern-matching compilation.Gravatar Hugo Herbelin2014-10-05
| | | | | | | | - Optimize the removal of generalization when there is no dependency in the generalized variable (see postprocess_dependencies, and the removal of dependencies in the default type of impossible cases). - Compute the onlydflt flag correctly (what allows automatic treatment of impossible cases even when there is no clause at all).
* STM: report the (structured) goals as XMLGravatar Carst Tankink2014-10-01
| | | | | The leafs of the XML trees are still pretty-printed strings, but this could be refined later on.
* Remove some 'deprecated' warnings.Gravatar Xavier Clerc2014-09-25
|
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
| | | | | | | Add a flag to indicate if we're in the toplevel or debuggger to not try to retype terms in the wrong environment (and making find_rectype, get_type_of untraceable). This fixes bug #3638 along with the previous commit.
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
|
* Undo: if the ui is coqtop (command line) then Undo is not part of the doc.Gravatar Enrico Tassi2014-09-09
|
* toploop plugins taken into account when printing --help (close: 3535)Gravatar Enrico Tassi2014-09-09
| | | | | | | | | | | | | E.g. Coq options are: -I dir look for ML files in dir -include dir (idem) [...] -h, --help print this list of options With the flag '-toploop coqidetop' these extra option are also available: --help-XML-protocol print the documentation of the XML protocol used by CoqIDE
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
|
* Adding a Ftactic module for potentially focussing tactics.Gravatar Pierre-Marie Pédrot2014-09-05
| | | | | | The code for the module was moved from Tacinterp. We still expose partially the implementation of the Ftactic.t type, for the sake of simplicity. It may be dangerous if used improperly though.
* coqworkmgrGravatar Enrico Tassi2014-09-02
|
* Type-safe version of genarg list / pair / opt functions.Gravatar Pierre-Marie Pédrot2014-08-29
|
* Simplification of Genarg unpackers.Gravatar Pierre-Marie Pédrot2014-08-29
| | | | | Instead of having a version of unpackers for each level, we use a dummy argument to force unification of types.
* Fixing bug #3541.Gravatar Pierre-Marie Pédrot2014-08-28
| | | | | | All superscript numbers are now symbols instead of parts of identifiers. This disallows some identifiers, but hopefully not a lot of people were using superscripts as part of identifiers, weren't they?
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
| | | | | | | | | | | It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
| | | | | par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
|
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
|
* Removing the call to Weak.get_copy in hashsets.Gravatar Pierre-Marie Pédrot2014-07-31
| | | | | | | | | | | | The rationale for its use comes from OCaml weak maps, and is justified by the fact that Weak.get may prevent its return value to be collected by the GC during the next slice even though nobody points to it. In our case, this is vastly irrelevant because hashconsed values are not expected to be collected whatsoever (save for exceptional cases). But Weak.get_copy is rather costly actually, at least strictly more than the plain Weak.get. Experimentally, I observe diminution of compilation time and even diminution of memory consumption (!) after this patch, so I assume it is a net gain.
* Improve intersection of regular trees.Gravatar Maxime Dénès2014-07-31
| | | | | For better efficiency, we try to preserve the shape of mutually recursive trees.
* Pp: only one default feedback idGravatar Enrico Tassi2014-07-29
|
* Pp compiles after feedbackGravatar Enrico Tassi2014-07-29
|
* Revert "Adding a "is_val" primitive to IStream."Gravatar Pierre-Marie Pédrot2014-07-24
| | | | This reverts commit 062d07eb5446c1032fda232b9a09e20e5410dd92.
* Refine check_is_subterm.Gravatar Maxime Dénès2014-07-22
| | | | | | | Following Bruno's suggestion, we check if the tree expected for the recursive argument is included in the one which is inferred. This check is probably not necessary in the current state of affairs, but might become so after further extensions of the guard condition.
* Made intersection on regular trees less intensional.Gravatar Maxime Dénès2014-07-22
|
* Refining match subterm and commutative cut rules. The parameters that areGravatar Maxime Dénès2014-07-22
| | | | | | instantiated in the return predicate are now taken into account. The resulting recargs tree is the intersection between the one of the branches and the appearing in the return predicate. Both the domain and co-domain are filtered.
* Adding a "is_val" primitive to IStream.Gravatar Pierre-Marie Pédrot2014-07-22
|
* Universe level maps use HMaps.Gravatar Pierre-Marie Pédrot2014-07-21
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 03:08:06 +0000