aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2013-04-23Remove deprecated option -no-hash-consing (currently doing nothing)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16442 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-19interface.mli and serialize.ml reworked to avoid copy/paste of typesgareuselesinge
With this commit the types involved in the protocol between Coq and Coqide are written once and for all in interface.mli serialize.ml is monkey code that contains a reified version of these types and the related machinery needed to marshal values in these types to/from xml in a modular way. This file should be automatically generated from the spec of the protocol in an ideal world. Phantom types are used to statically check that the reified form of the types is in sync with the one declared in interface.mli The benefit of this commit is that changing the protocol is easier: one changes the types in interface.mli and lets ocamlc spot all the places that needs to be modified. This is a necessity if one plays with the protocol very often, like in my Paral-ITP branch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16438 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-16More in IArrayppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16408 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-15votour: a small tool for guided tours of .voletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16403 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
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
2013-04-09Added a module of immutable arrays. Not as full as CArray, but shouldppedrot
be soon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16391 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-23Minor code cleaning in CArray / CList.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Removing mandatory suffixes for library files.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-17Checker: simplify a bit its exception handlerletouzey
We use Errors.print for anomalies and other uncaught exceptions in the checker: this should print the same message, it is shorter this way, and we avoid using Errors.is_anomaly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16310 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-14Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncriticalletouzey
This was apparently already the case before, but this invariant is now explicited in comments + a few asserts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16305 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Made the backtrace type opaqueppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16298 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Vernac+Toplevel: get rid of Error_in_fileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16294 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 5)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16281 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 4)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16280 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12New function Errors.noncritical for restricting try ... with ...letouzey
For the moment, are considered critical : Sys.Break, Stack_overflow, Out_of_memory Assert_failure, Match_failure, Anomaly, Timeout, Drop, Exit These exceptions should normally *not* be catched by a "try", hence the suggested code for generic "try": try ... with e when Errors.noncritical e -> ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16269 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Updated Exninfo to the new Store type.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16268 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Allowing different types of, not to be mixed, generic Stores throughppedrot
functor application. Rewritten the interface btw. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16267 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-05More monomorphization.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-05Missing primitive in CArrayppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16259 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-24New -no-native-compiler flag for configure, globally disabling the nativemdenes
compiler (implemented on Matthieu's request). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16240 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
mechanism to retrieve the same information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16215 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Adding more primitives to Exninfoppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16214 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Updating the backtrace handling mechanism to accomodate the newppedrot
exception information addition facility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16213 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Added exception enrichment. Now one can define additional arbitraryppedrot
information worn by exceptions. The implementation is quite hackish but it should work nonetheless. Basically, it adds an additional cell to exceptions arguments, in which you can put whatever you want. By typing invariants, you may not reach this cell by normal means, so it should be safe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16212 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-01v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16183 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Actually adding backtrace handling.ppedrot
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
2013-01-28Added backtrace primitives.ppedrot
Using OCaml 3.11+ builtin facilities to record stack frames during exception raising, we can now recover at runtime the backtrace of an uncaught toplevel exception and display it to the user, without the infamous OCaml debugger. The backtrace is displayed when using the [-debug] flag. This requires a bit of discipline, as each time we reraise an exception we need to keep track of those frames we discarded between the previous raise and the current [try-with] branch. Currently, only [Anomaly] is handled, but this can be ported to any exception as long as we add the backtrace info into the exception, and we provide the corresponding handler to [Backtracke.register_backtrace_handler]. Hopefully this should not be to costly, as we only do little work when reraising, and only with the [-debug] flag set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16166 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Uniformization of the "anomaly" command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Added backtrace information to anomaliesppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16161 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
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
2013-01-12Envar: in w32, add .exe when searching for caml binariesletouzey
Based on a patch by Pierre-Yves Strub git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16124 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-19Array.create is deprecatedpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16104 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-19Fix coqtop -config when absolute path have been given for ocaml*pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16102 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Moving hcons_string to String namespace.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16069 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16068 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-13Documented CString.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16064 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16063 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-08Ensure that a function declared with a label is used with itletouzey
This correspond to ocaml4 warning 6 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16053 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-08Removed a unused function in Ppppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16048 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07Envars: repair failed compilation after yann's commitsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16040 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07* lib/Envars:regisgia
Beautify. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16031 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07* lib/Envars:regisgia
- Document interface file. - Now export references to ocaml compilers used to compile Coq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16030 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-25More equality functionsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15998 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-22Monomorphization (lib)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15991 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-20Cleaning and small optimization in CList.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15988 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-19Serialize: no need anymore to export of_value / to_value in the mliletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15986 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-17 02:48:05 +0000