| Age | Commit message (Collapse) | Author |
|---|
|
Detected incidentally in "validate" check for #8893.
|
|
on test-suite/arithmetic/mod: 2.6s to 0.45s
|
|
About 20% better perf on test-suite/arithmetic/mod (3.4s to 2.6s)
|
|
For instance this halves the time it takes to check
the test-suite/arithmetic/ files.
on mod: 7.5s to 3.4s
|
|
Prevent errors when under annotating binders.
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
This library is private and shouldn't be exposed to plugins.
|
|
It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.
Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.
|
|
Reviewed-by: Zimmi48
|
|
The `-boot` option was used to:
- suppress loading of the rc_file
- allow to save modules with prefix `Coq`
There is no good reason disable saving of modules with `Coq` prefix by
default, thus we remove this option.
Fixes: #9575
|
|
In passing add -coqlib to coqchk's usage message.
|
|
+ remove checker/.depend forgotten file
|
|
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
|
|
I think the usage looks cleaner this way.
|
|
Instead, if the coqlib is special, we set it explicitly in the command
line, as Dune does.
This is a continuation of #9523.
In Sphinx, we stop using -boot, and pass `-coqlib` through the
environment instead.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
|
|
comments.
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id.
Remove the ability to split the argument of `Univ.Level.Level` into a
dirpath*int pair (except by going through string hacks like
detyping/pretyping(/funind) does).
Id.of_string_soft to turn unnamed universes into qualid is pushed up
to detyping. (TODO some followup PR clean up more)
This makes it pointless to have an opaque type for ints in
Univ.Level: it would only be used as argument to
Univ.Level.UGlobal.make, ie
~~~
open Univ.Level
let x = UGlobal.make dp (Id.make n)
(* vs *)
let x = UGlobal.make dp n
~~~
Remaining places which create levels from ints are various hacks (eg
the dummy in inductive.ml, the Type.n universes in ugraph
sort_universes) and univgen.
UnivGen does have an opaque type for ints used as univ ids since they
get manipulated by the stm.
NB: build breaks due to ocamldep issue if UGlobal is named Global instead.
|
|
Remote counters were trying to build universe levels (as opposed to
simple integers), but did not have access to the right dirpath at
construction time. We fix it by constructing the level only at use time,
and we introduce some abstractions for qualified and unqualified level
names.
|
|
|
|
|
|
|
|
|
|
|
|
Now that we link lib we can do this.
|
|
|
|
As far as I can tell this is similar to what coqtop does. Delta
resolvers are complicated so I may be mistaken.
The important part is to avoid losing the modified delta resolver
returned by strengthen_and_subst in check_mexpr.
|
|
|
|
|
|
Now that the checker shares code with the kernel using md5 cic.mli
doesn't work. We could md5 declarations.ml but this would miss changes
to constr (and cic.mli already missed changes to names, univs).
Instead we just print a bit of information (the last seen type
name/annotation) when validate fails. This should help debugging when
forgetting to update values.ml without the full verbosity of -debug.
As such there is no need to -debug in the makefile validate
target (NB: CI has an independent implementation of the validate rule
since the vos are installed there).
|
|
This allows to use the nice printers with constrextern etc, and since
we were copying everything we're not linking any more than previously.
Also the dune file is simpler without the copies.
|
|
|
|
There is little point in having a list, as there is virtually no sharing
nor expansion of bound universe names. This representation is thus more
compact.
|
|
|
|
|
|
At the same time, we made the safe_env threading explicit.
|
|
|
|
|
|
For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.
With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.
We also rename some files from the checker so that they don't clash with
kernel files.
|
