| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
Kudos to PMP for spotting that!
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
non-ML applications. Control channel can be also ignored.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
- 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.
|
| | |
|
| | |
|
| |
|
|
|
| |
These modules are not as reusable as one may want them to be, but
moving them out simplifies a little STM.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
| |
(hopefully), and forbids generic equality. Still, it allows generic hash.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
the provided type to come with a hashing function. The internal representation
is changed, such that values are first compared w.r.t. to their hash.
This effectively saves a lot of comparisons which may be far more expensive
than O(1), as in the string case, hence resulting in an overall speedup.
CAVEAT: everything is not implemented yet, and order-sensitive functions
now do not respect the provided order anymore.
|
| |
|
|
| |
The removed code isn't used locally and isn't exported in the signature
|
| |
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Anyway, a few syntactic features of 3.12 were already used here and
there (e.g. local opening via Foo.(...), or the record shortcut
{ field; ... }). Hence compiling with 3.11 wasn't working anymore.
Already take advantage of the following 3.12.1 features :
- "module type of ..." in CArray, CList, CString ...
- "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output
via our coqdep to localize the .ml4 modules :-)
The -ml-synonym option (+ various bugfixes) is the reason for asking
3.12.1 directly and not just 3.12.0. After all, if debian stable is
providing 3.12.1, then everybody has it ;-)
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
| |
Introducing List.fold_right and List.fold_left in Monad.
|
| |
|
| |
Adds a combinator List.map_right which chains effects from right to left.
|
| |
|
| |
This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
|
| |
|
|
|
| |
When you resume the compilation of a .vi file, you want to
avoid collisions on fresh names.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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).
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
Two changes:
- 'a Lazy.t becomes unit -> 'a
- 'a t becomes 'a u (the view type)
This spares two Lazy.force, and leverages Lazy.lazy_from_fun. Considering Lazy.force is fairly slow, in particular because of the write-barrier, this should be beneficial.
|
| |
|
| |
Lazy.lazy_from_val does almost the same thing as this Obj.magic. It makes some extra dynamic check, but it's frankly unlikely that it could be observed.
|
| |
|
| |
View types are better practice than option types for pattern-matching. (Plus, they save a minute amount of allocations)
|
| | |
|
| |
|
|
|
| |
nasty relating memory management triggering random segfaults. But this seemed
really unlikely...
|
| |
|
|
|
| |
1. Only apply last Zupdates
2. Better smartmap with state.
|
| | |
|
| | |
|
| |
|
|
| |
Moreover, cleanup of System.connect (used by the "external" tactic).
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
Enrico Tassi
Pierre-Marie Pédrot
Carst Tankink
Guillaume Melquiond
Virgile Prevosto
Pierre Letouzey
Pierre Boutillier
Arnaud Spiwack