| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
The command `coqtop -check-vi-tasks 1,4,2 a` checks tasks 1 4 2,
in this precise order, stored in a.vi.
The command `coqtop -schedule-vi-checking 4 a b c` reads {a,b,c}.vi
and .{a,b,c}.aux and spits 4 command lines to check all the tasks in
{a,b,c}.vi trying to equally partition the job between the 4 workers,
that can indeed be run in parallel.
The aux file contains the time that it took to check the proofs stored
in the .vi files last time the file was fully checked.
This user interface is still very rough, it should probably run the
workers instead of just printing their command line.
|
|
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
|
|
To make this possible the state id has to reach the kernel.
Hence definition_entry has an extra field, and many files had
to be fixed.
|
|
When using libraries I find it convenient (and future proof) to use fully qualified paths in many places. It would be nice to have a convenient short-hand for this so that you can:
From Xxx Require Yyy Zzz.
instead of having to type:
Require Xxx.Yyy Xxx.Zzz.
Signed-off-by: Pierre Boutillier <pierre.boutillier@ens-lyon.org>
|
|
|
|
|
|
|
|
anomaly is raised. As there are very few tags defined in Coq code, this is
very unlikely to appear, and can be fixed by tweaking the name of the
dynamic argument.
This should be more efficient, as we did compare equal strings each time.
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17067 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17066 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@16944 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
To reduce the amount of syntactic noise, we now provide
a few inner modules Int.List, Id.List, String.List, Sorts.List
which contain some monomorphic (or semi-monomorphic) functions
such as mem, assoc, ...
NB: for Int.List.mem and co we reuse List.memq and so on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16922 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 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@16890 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
with OCaml 3.12.1).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Just sufficient to make abstract work in such an (empty) lib.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16772 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This summary entry is special because its unfreeze may load ML
code that in turns adds summary entries. Hence it is the first
summary piece to be unfreezed, otherwise some summaries may get
lost.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16752 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
|
|
The Stm commit switched from an home made handling of failures to
a with_state_protection. This was wrong, since in case of success
the global state has to be left altered.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16746 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The extended signature is defined in CMap, and should be compatible
with the old one, except that module arguments have to be explicitely
named. The implementation itself is quite unsafe, as it relies on the
current implementation of OCaml maps, even though that should not be
a problem (it has not changed in ages).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16725 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Since digests are strings (of size 16), we just dump them
now in vo files (cf. Digest.output) instead of using Marshal
on them : this is cleaner and saves a few bytes.
Increased VOMAGIC to clearly identify this change in the format.
Please rerun ./configure after this commit.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 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
|
|
Non-opaque-constant's side effects are processed before
the constant enters the kernel and global constants are
generated for them (as before, but not by side effect in
the middle of the proof construction).
This makes sense because proofs ending with Defined have
to be run immediately, so the list of side effects is
immediately available.
These side effects are type checked again.
To fix that the idea of kernel signatures could be employed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16702 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16679 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@16659 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
When refering to a module / module type, or when doing an include,
we do not duplicate and substitution original libobjects immediatly.
Instead, we store the module path, plus a substitution. The libobjects
are retrieved later from this module path and substituted, typically
during a Require. This allows to vastly decrease vo size (up to 50%
on some files in the stdlib). More work is done during load (some
substitutions), but the extra time overhead appears to be negligible.
Beware: all subst_function operations should now be
environment-insensitive, since they may be arbitrarily delayed.
Apparently only subst_arguments_scope had to be adapted.
A few more remarks:
- Increased code factorisation between modules and modtypes
- Many errors and anomaly are now assert
- One hack : brutal access of inner parts of module types
(cf handle_missing_substobjs)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16630 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16629 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16627 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
When arguments scopes are set manually, nothing new, they stay
as they are (until maybe another Arguments invocation).
But when argument scopes are computed out of the argument type and
the Bind Scope information, this kind of scope is now dynamic:
a later Bind Scope will be able to impact the scopes of an earlier
constant. For Instance:
Definition f (n:nat) := n.
About f. (* Argument scope is [nat_scope] *)
Bind Scope other_scope with nat.
About f. (* Argument scope is [other_scope] *)
This allows to get rid of hacks for modifying scopes during functor
applications. Moreover, the subst_arguments_scope is now
environment-insensitive (needed for forthcoming changes in declaremods).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 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@16510 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16502 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16501 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
it into the standard logger instead.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
States.freeze takes ~marshallable:bool, so that (only) when we want to
marshal data to disk/network we can ask the freeze functions of the
summary to force lazy values. The flag is propagated to Lib and Summary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16478 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
One can freeze/unfreeze a portion of the summary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16477 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
1. sorts.ml: A small file utility for sorts;
2. constr.ml: Really low-level terms, essentially kind_of_constr, smart
constructor and basic operators;
3. vars.ml: Everything related to term variables, that is, occurences
and substitution;
4. context.ml: Rel/Named context and all that;
5. term.ml: derived utility operations on terms; also includes constr.ml
up to some renaming, and acts as a compatibility layer, to be deprecated.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
|
