| Age | Commit message (Collapse) | Author |
|---|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
|
|
|
|
This operation is done directly in Safe_typing.register_inline and has
nothing to do with retroknowledge afaict.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and
kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program
rather than a pipeline of sed and awk text processing.
|
|
|
|
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.
|
|
|
|
|
|
|
|
The strategy is to backtrack when a constant is in head
position: we first try to see if the arguments are guarded,
if not we unfold.
Since `Case` is represented as a head (rather than as a context
as the reduction machine does) we did not backtrack there
and reduce (including delta) the scrutinized in order to
fire the iota redex.
This commit adds a choice point in that specific case, and
reduces eagerly (not step by step) the scrutinized in case
of failure.
|
|
I think the usage looks cleaner this way.
|
|
|
|
|
|
records
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
In order for Dune to work in Windows we need to tweak some script
calls, they need a POSIX shell and the `(run ...)` / `(system ...)`
actions use `cmd.exe` on Windows.
Hopefully, we will rely less on `bash` when Dune can understand Coq
libraries. This affects shell scripts in `kernel/**.sh` for example.
It is interesting to see how faster the Coq Windows build is with Dune
+ Windows.
There are some problems with PATHs that prevent the test suite from
working, these will be fixed in a future PR.
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
|
|
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>
|
|
|
|
Fix #8076.
|
|
This simplifies reasoning about the kernel code.
We still auto downgrade squashed Prop records as the code path to
avoid an error is more involved. Alternatively we could produce an
error forcing people to Unset Primitive Projections if they want a
squashed record.
|
|
We split into smaller functions, use more specific types for universe
manipulation, and try to limit how much of the big tuple gets passed
to subroutines.
|
|
This is strictly code movement.
|
|
|
|
In passing, slightly unify the API to make it clearer.
|
|
It seems that it was a remnant of a time where Reductionops would share the
same data types.
|
|
|
|
This should give better visibility of universe specific operations vs
generic graph operations.
|
|
We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`]
CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit`
cannot be currently installed, thus we have to add a switch to the
test suite to disable `unit-tests`.
Many deprecation warnings happened in 4.08 so we use the `release`
profile to make them not fatal. Using a 4.08 build profile would be an
option too.
|
|
|
|
|
|
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.
|
|
|
|
|
|
When making a universe a variable we iterate through the universes
we're equal to and if we find one we update the substitution
accordingly.
NB: The bug called make_flexible_variable on Top.15 and
~~~
{Top.15 Top.14} |= Top.11 < Top.6
Top.14 < Top.5
Top.11 = Top.15
ALGEBRAIC UNIVERSES:{Top.17 Top.16}
UNDEFINED UNIVERSES:Top.17 := Top.14+1
Top.16 := Top.14+1
WEAK CONSTRAINTS:
~~~
so now we would add [Top.15 := Top.11].
|
|
|
|
|
|
`clib` doesn't need `dynlink`, but `lib` does, similarly for
`threads`, `num`...
We align Dune and META deps.
|
|
|
|
cleanups
|
|
|
|
|
|
|
|
The use of a term is not needed for the fast typing algorithm of the
application case, so this tweak brings the best of both worlds.
|
