| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
Instead of considering all constants without body in the environment,
consider only the ones appearing in the body of the opacified constant.
|
|
When encountering
```Coq
Module M : T.
...
Lemma c :...
...
Qed.
...
End M.
```
every field `c` without body in `T` but with a body in `M` is
registered as opacified in a table along with all constants
`opacified(c)` without body in the environment at this point (i.e.,
all axioms potentially used by c).
Then, when printing axioms, if `c` appears in the final environment it
is replaced by `opacified(c)` in the resulting list of axioms.
|
|
|
|
We tweak the message a bit.
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
See CEP#44 for futher details.
|
|
|
|
|
|
|
|
|
|
|
|
Add headers to a few files which were missing them.
|
|
|
|
This could have been at the root of strange behaviours (read unsoundness).
|
|
For an inductive block to be template, all its components must also
be. This is probably fixing a few soundness bugs in the process, but I
do not want to think too much about it.
|
|
|
|
data from a part where it should never access it.
|
|
This was the only part in the kernel that really relied on the contents
of the Monomorphic node.
|
|
And enable related test.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
|
|
preparation for direct discharge
|
|
representation.
Reviewed-by: maximedenes
|
|
It gets thrown away if the inductive is declared in a section anyway,
and there is no user syntax to specify it.
|
|
dune-dbg depends on coqchk.bc and coqide_main.bc, and apparently they
now need explicit modes to be produced.
|
|
It seems this passed under my radar, but the change of implementation of the
safe demarshaller introduced by native integers and floating point numbers is
dangerous.
For floats, it makes the demarshaller depend on float kernel representation.
This is just an alias to the standard OCaml float type, so this is currently
not problematic, but this makes the code fragile if ever we decide to change
it there. This would trigger unsound object casts without any complaint from
the type-checker. Furthermore, having such a low-level library depend on
the kernel library sounds like a anti-feature to me.
For native integers, the situation is direr. The demarshaller turns
unconditionally 64-bits integers into their Int63 representation, which
depends on the architecture. This means that when parsing vo files from
a architecture where these types are not the same, we are guaranteed to get
into unsound casts. Some of them *might* get caught by the value
representation checker, yet it is a footgun. The demarshaller should only
deal with OCaml representations and not try to mess with Coq specific
data types, otherwise we are going to face desynchronization and thus
unsound casts.
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
* Add a related test-suite in compare.v (generated by a bash script)
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
|
|
|
|
|
|
|
|
|
|
`Import` does not actually need to register an object, only `Export`
does. So we specialize and rename the object into `ExportObject`.
|
|
Libraries are now handled like other modules.
|
|
This could be Prop (for compat with usual Coq), Set (for HoTT),
or actually an arbitrary "i".
Take lower bound of universes into account in pretyping/engine
Reinstate proper elaboration of SProp <= l constraints:
replacing is_small with equality with lbound is _not_ semantics preserving!
lbound = Set
Elaborate template polymorphic inductives with lower bound Prop
This will make more constraints explicit
Check univ constraints with Prop as lower bound for template inductives
Restrict template polymorphic universes to those not bounded from below
Fixes #9294
fix suggested by Matthieu
Try second fix suggested by Matthieu
Take care of modifying elaboration for record declarations as well.
Rebase and export functions for debug
Remove exported functions used while debugging
Add a new typing flag "check_template" and option "-no-template-checl"
This parameterizes the new criterion on template polymorphic inductives
to allow bypassing it (necessary for backward compatibility).
Update checker to the new typing flags structure
Switch on the new template_check flag to allow old unsafe behavior in
indTyping.
This is the only change of code really impacting the kernel, together
with the commit implementing unbounded from below and parameterization
by the lower bound on universes.
Add deprecated option `Unset Template Check` allowing to make proof
scripts work with both 8.9 and 8.10 for a while
Fix `Template Check` option name and test it
Add `Unset Template Check` to Coq89.v
Cooking of inductives and template-check tests
Cleanup test-suite file for template check / universes(template) flags
cookind tests
Move test of `Unset Template Check` to the failure/ dir, but comment it
for now
Template test-suite test explanation
Overlays for PR 9918
Overlay for paramcoq
Add overlay for fiat_parsers (-no-template-check)
Add overlay for fiat_crypto_legacy
Update fiat-crypto legacy overlay
Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made.
Remove overlay that should no longer be necessary
The setting in the compat file should handle it
Remove now-merged fiat-crypto-legacy overlay
Update `Print Assumptions` to reflect the typing flag for template checking
Fix About and Print Assumptions for template poly, giving info on which
variables are actually polymorphic
Fix pretty printing to print global universe levels properly
Fix printing of template polymorphic universes
Fix pretty printing for template polymorphism on no universe
Fix interaction of template check and universes(template) flag
Fix indTyping to really check if there is any point in polymorphism: the
conclusion sort should be parameterized over at least one local universe
Indtyping fixes for template polymorphic Props
Allow explicit template polymorphism again
Adapt to new indTyping interface
Handle the case of template-polymorphic on no universes
correctly (morally Type0m univ represented as Prop).
Fix check of meaningfullness of template polymorphism in the kernel.
It is now done w.r.t the min_univ, the minimal universe inferred for the
inductive/record type, independently of the user-written annotation
which must only be larger than min_univ. This preserves compatibility
with UniMath and template-polymorphism as it has been implemented up-to
now.
Comment on identity non-template-polymorphism
Remove incorrect universes(template) attributes from ssr
simpl_fun can be meaningfully template-poly, as well as
pred_key (although the use is debatable: it could just
as well be in Prop).
Move `fun_of_simpl` coercion declaration out of section to respect
uniform inheritance
Remove incorrect uses of #[universes(template)] from the stdlib
Extraction of micromega changes due to moving an ind decl out of a section
Remove incorrect uses of #[universes(template)] from plugins
Fix test-suite files, removing incorrect #[universes(template)] attributes
Remove incorrect #[universes(template)] attributes in test-suite
Fix test-suite
Remove overlays as they have been merged upstream.
|
|
Instead of doing (simplified code)
~~~ocaml
let check env kn cb =
let flags = env.flags in
let env' = set_flags env cb.flags in
...
let env = add_constant cb kn (if poly then env else env') in
set_flags env flags
~~~
(NB: when not poly env' has only the typing flags different from env)
we do
~~~ocaml
let check env kn cb =
let env = set_flags env cb.flags in
...
()
let check env kn cb =
let () = check env kn cb in
add_constant cb kn env
~~~
|
|
Now all relevant typing_flags are taken in account by the checker.
The different forms of assumptions are now printed by the checker.
|
|
(co)fixpoints) and [check_positive] (for (co)inductive types).
|
|
The changes are large due to `Pervasives` deprecation:
- the `Pervasives` module has been deprecated in favor of `Stdlib`, we
have opted for introducing a few wrapping functions in `Util` and
just unqualified the rest of occurrences. We avoid the shims as in
the previous attempt.
- a bug regarding partial application have been fixed.
- some formatting functions have been deprecated, but previous
versions don't include a replacement, thus the warning has been
disabled.
We may want to clean up things a bit more, in particular
w.r.t. modules once we can move to OCaml 4.07 as the minimum required
version.
Note that there is a clash between 4.08.0 modules `Option` and `Int`
and Coq's ones. It is not clear if we should resolve that clash or
not, see PR #10469 for more discussion.
On the good side, OCaml 4.08.0 does provide a few interesting
functionalities, including nice new warnings useful for devs.
|
|
We make a few libobject constructions (Module, Module Type,
Include,...) first-class and rephrase their handling in direct style (removing
the inversion of control). This makes it easier to define iterators over
objects without hacks like inspecting the tags of dynamic objects.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
