| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
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)
|
|
|
|
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.
|
|
|
|
|
|
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).
|
|
Impacts MapleMode.
|
|
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.
|
|
|
|
This changes the tacinterp API, but only affects (one line of) the MapleMode contrib.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
That was a bug. coqc a b was generating (for b) an opaque table containing
also the proofs of a.
|
|
This meas that the list of future_constraints in safe_env is empty,
meaning that nothing was delayed.
|
|
|
|
|
|
Make this module deal only with opaque proofs.
Make discharging/substitution invariant more explicit via a third constructor.
|
|
|
|
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).
|
|
|
|
|
|
discrepancy introduced in commit d3eac3d5fc8e5af499eb8750ca08ead8562dac6f
|
|
discrepancy introduced in commit 400327165edcba667ebb70ebb89052455656b719
|
|
|
|
|
|
It fixes micromega. It is frankly a mystery to me why psatz ever work. The semantics of Ltac's match is still fishy.
|
|
|
|
I'm trying to avoid unecessary construction of intermediate lists. Interpretation function don't modify the goals, they just need a goal in their
context.
Some care has to be given to the evar maps, though, as we can extract an outdated evar map from a goal (this is probably an undesirable feature, but significantly simplified the compatibility API).
Also, Proofview.Goal.enter{,l} catch exceptions (and transfer the non-critical ones into errors of the tactics monad). So I had to do just that for every "enter" removed (I probably have been overprotective but it's better that way).
Not as trivial a modification as it should, but it will hopefully go over well. It was much needed anyway.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
