| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Inside a section, Let followed by a Proof. Qed. are handled as regular
definitions, hence they have universe constraints coming from the type
and from the body. Only the former set was returned to libstack, but
both sets were added to the global universe graph. Hence, at section
closing time, an incomplete set of universe constraints was added back
to the global graph (End Section replays the libstack) and hence saved
in the .vo file. coqchk was right in reporting missing constraints.
|
|
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).
|
|
Universe constraints coming from subtyping were not propagated
to the outermost module and hence not stocked in the .vo file.
Still, they were added to the interactive safe environment and
hence checked for satisfiability.
|
|
iter order, but it seems nobody was relying on it (contrarily to the string case).
|
|
|
|
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.
|
|
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).
|
|
File format:
The .vo file format changed:
- after the magic number there are 3 segments. A segment is made of 3
components: bynary int, an ocaml value, a digest. The binary int
is the position of the digest, so that one can skip the value without
unmarshalling it
- the first segment is the library, as before
- the second segment is the STM task list
- the third segment is the opaque table, as before
A .vo file has a complete opaque table (all proof terms are there).
A .vi file follows the same format of a .vo file, but some entries
in the opaque table are missing. A proof task is stocked instead.
Utilities:
coqc: option -quick generates a .vi insted of a .vo
coq_makefile: target quick to generate all .vi
coqdep: generate deps for .vi files too
votour: can browse .vi files too, the first question is which segment
should be read
coqchk: rejects .vi files
|
|
Let proof terms are stocked in the named_context that is used directly
everywhere, hence there is no way to stock a Future proof term there.
|
|
For now, this reference (renamed to link_info) has been moved to the
environment (for constants and inductive types). But this is only a first step
towards making the native compiler more functional.
|
|
Also, the future chain that reaches the kernel is greedy.
If the user executes step by step, then the error is raised immediately.
|
|
This optimization was undone because the kernel type checking was
not a pure functions (it was accessing the conv_oracle state imperatively).
Now that the conv_oracle state is part of env, the optimization can be
restored. This was the cause of the increase in memory consumption, since
it was forcing to keep a copy of the system state for every proof, even the
ones that are not delayed/delegated to slaves.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16963 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
But for vm, the kernel should be functional now
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
A future always carries a fix_exn with it: a function that enriches
an exception with the state in which the error occurs and also a safe
state close to it where one could backtrack.
A future can be in two states: Ongoing or Finished.
The latter state is obtained by Future.join and after that the future
can be safely marshalled.
An Ongoing future can be marshalled, but its value is lost. This makes
it possible to send the environment to a slave process without
pre-processing it to drop all unfinished proofs (they are dropped
automatically in some sense).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16845 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
If a constant is defined as transparent, not only its side effects
(opaque sub proofs as in abstract, and transparent ind schemes)
are declared globally, but the ones that are schemes are also declared
as such.
The only sub optimal thing is that the code handling in a special
way the side effects of transparent constants is in declare.ml that
does not see ind_tables.ml, hence a forward ref to a function is used.
IMO, ind_tables has no reason to stay in toplevel/.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16747 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16741 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The earlier type [struct_expr_body] was far too broad,
leading to code with unclear invariants, many "assert false", etc etc.
Its replacement [module_alg_expr] has only three constructors:
* MEident
* MEapply : note the module_path as 2nd arg, no more constraints here
* MEwith : no more constant_body inside, constr is just fine
But no more SEBfunctor or SEBstruct constructor here (see below).
This way, this datatype corresponds to algebraic expressions,
i.e. anything that can appear in non-interactive modules.
In fact, it even coincides now with [Entries.module_struct_entry].
- Functor constructors are now necessarily on top of other
structures thanks to a generic [functorize] datatype.
- Structures are now separated from algebraic expressions by design :
the [mod_type] and [typ_expr] fields now only contain structures
(or functorized structures), while [mod_type_alg] and [typ_expr_alg]
are restricted to algebraic expressions only.
- Only the implementation field [mod_expr] could be either algebraic
or structural. We handle this via a specialized datatype
[module_implementation] with four constructors:
* Abstract : no implementation (cf. for instance Declare Module)
* Algebraic(_) : for non-interactive modules, e.g. Module M := N.
* Struct(_) : for interactive module, e.g. Module M : T. ... End M.
* FullStruct : for interactive module with no type restriction.
The [FullStruct] is a particular case of [Struct] where the implementation
need not be stored at all, since it is exactly equal to its expanded
type present in [mod_type]. This is less fragile than hoping as earlier
that pointer equality between [mod_type] and [mod_expr] will be
preserved...
- We clearly emphasize that only [mod_type] and [typ_expr] are
relevant for the kernel, while [mod_type_alg] and [typ_expr_alg]
are there only for a nicer extraction and shorter module printing.
[mod_expr] is also not accessed by the kernel, but it is important
for Print Assumptions later.
- A few implicit invariants remain, for instance "no MEwith in mod_expr",
see the final comment in Declarations
- Heavy refactoring of module-related files : modops, mod_typing,
safe_typing, declaremods, extraction/extract_env.ml ...
- Coqchk has been adapted accordingly. The code concerning MEwith
in Mod_checking is now gone, since we cannot have any in mod_expr.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16712 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- No more modinfo sub-record in the safe_environment record,
this was a syntactic pain.
senv.modinfo.modpath --> senv.modpath
senv.modinfo.variant --> senv.modvariant
senv.modinfo.resolver --> senv.modresolver
senv.modinfo.resolver_of_param --> senv.paramresolver
senv.modinfo.label : removed (can be inferred from modpath)
- No more systematic chaining of safe_environment ('old' field).
Instead, earlier safe_environment is stored in the modvariant field
when necessary (STRUCT and SIG case).
- Improved sharing between end_module and end_modtype
- More qualified names instead of open, better comments, ...
- Some user errors are now checked earlier elsewhere (see for
instance vernac_end_segment), so we can turn these errors into
asserts. The user error about higher-order include is now algebraic.
- Highlight the idea of a state monad in Safe_typing :
type 'a safe_transformer = safe_environment -> 'a * safe_environment
More systematic code in Global, thanks to 'globalize' function.
- Declaremods : less informations stored in openmod_info
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16708 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In some cases, an 'a -> 'b field is changed into an ('a -> b') option
field so that one can forget the closures and marshal the resulting
state
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16683 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It can be:
`Yes Full data, in a state that can be marshalled
`No Full data, good for Undo only
`Shallow Partial data, marshallable, good for slave processes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16682 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The process_transaction function adds a new edge to the Dag without
executing the transaction (when possible).
The observe id function runs the transactions necessary to reach to the
state id. Transaction being on a merged branch are not executed but
stored into a future.
The finish function calls observe on the tip of the current branch.
Imperative modifications to the environment made by some tactics are
now explicitly declared by the tactic and modeled as let-in/beta-redexes
at the root of the proof term. An example is the abstract tactic.
This is the work described in the Coq Workshop 2012 paper.
Coq is compile with thread support from now on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16628 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
the VM
too. Almost only a new grammar entry since the inlining machinery was already
implemented.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16623 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16502 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- get_module_substobjs (resp. modtype) without useless mp_from arg
- no need for the whole Safe_typing.pack_module
- ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16407 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Get rid of the LightenLibrary hack : no more last-minute
collect of opaque terms and Obj.magic tricks. Instead, we
make coqc accumulate the opaque terms as soon as constant_bodies
are created outside sections. In these cases, the opaque
terms are placed in a special table, and some (DirPath.t * int)
are used as indexes in constant_body. In an interactive session,
the local opaque terms stay directly stored in the constant_body.
The structure of .vo file stays similar : magic number, regular
library structure, digest of the first part, array of opaque terms.
In addition, we now have a final checksum for checking the
integrity of the whole .vo file. The other difference is that
lazy_constr aren't changed into int indexes in .vo files, but are
now coded as (substitution list * DirPath.t * int). In particular
this approach allows to refer to opaque terms from another
library. This (and accumulating substitutions in lazy_constr)
seems to greatly help decreasing the size of opaque tables :
-20% of vo size on the standard library :-). The compilation times
are slightly better, but that can be statistic noise.
The -force-load-proofs isn't active anymore : it behaves now
just like -lazy-load-proofs. The -dont-load-proofs mode has
slightly changed : opaque terms aren't seen as axioms anymore,
but accessing their bodies will raise an error.
Btw, API change : Declareops.body_of_constant now produces directly
a constr option instead of a constr_substituted option
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16382 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Very little space saved this way, but it would hurt either...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16375 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16374 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16253 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml
- the functions that were in declarations.ml (mostly substitution utilities
and hashcons) are now in kernel/declareops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16249 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Ok, this is merely a matter of taste, but up to now the usage
in Coq is rather to use capital letters instead of _ in the
names of inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16153 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16098 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15992 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Util module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15802 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
compiler warnings).
I was afraid that such a brutal refactoring breaks some obscure
invariant about linking order and side-effects but the standard
library still compiles.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We now accept the following code: Definition E := 0. Module E. End E.
Techically, we simply allow the same label to occur at most twice in
a structure_body, which is a (label * structure_field_body) list).
These two label occurences should not be at the same level of fields
(e.g. a SFBmodule and a SFBmind are ok, but not two SFBmodule's or
a SFBmodule and a SFBmodtype). Gain : a minimal amount of code change.
Drawback : no more simple List.assoc or equivalent should be performed
on a structure_body ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15088 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
