| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
|
|
Ack-by: ejgallego
Reviewed-by: gares
|
|
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: vbgl
Reviewed-by: cpitclaudel
|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
documentation.
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
|
|
Reviewed-by: gares
|
|
registered in futures
Ack-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
As far as I understood, this was useful for tine-tuning the stm but
this is no longuer needed: it is ok not to have exception handler when
a constant registration does not span over several commands (such as
"Goal ... Qed" or obligations).
|
|
Reviewed-by: ejgallego
Ack-by: SkySkimmer
Ack-by: gares
Ack-by: jfehrle
Ack-by: vbgl
|
|
|
|
specific branch.
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: maximedenes
Reviewed-by: vbgl
|
|
Reviewed-by: Zimmi48
Ack-by: rgrinberg
|
|
|
|
As requested by Gaëtan Gilbert, we add shims
- `dev/shim/coqtop-prelude`
- `dev/shim/coqide-prelude`
that will build and start `coqtop` and `coqide` with just the prelude
loaded properly.
`dune exec dev/shim/coqtop-prelude` will build and execute this shim,
equivalent to doing `make states && bin/coqtop` under the old model.
This PR is just a bit of "a hack" until proper support for Coq
libraries arrives to Dune, however there is nothing wrong with it.
In particular, we must bootstrap `coq.plugins.ltac` as Dune needs to
compute the full installation path to allow `%{bin:foo}` in deps,
[this is a kind of shortcoming of the current implementation, and the
error message is just terrible]
We cannot depend on installed `.vo` files without doing a gross hack
[including them inside an ml lib] so for now we just depend on their
non-installed forms. Using `%{bin}` is good enough for the shims who
would like to locate binaries using `PATH`.
The long term plan (for now) is to have a command similar to `dune
utop $dir`, `dune coqtop $dir`, which would spawn a proper Coq shell
with the corresponding libraries on the path.
This will work for `dir=stdlib/Init/` for example, or for any other
combination.
|
|
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
Ack-by: rgrinberg
Ack-by: vbgl
|
|
Reviewed-by: ejgallego
|
|
|
|
This should allow CI jobs that use our Cachix to only test against Coq versions
that are already available in Cachix, avoiding very long build and time outs e.g.
in the math-classes CI.
Co-authored-by: Vincent Laporte <Vincent.Laporte@inria.fr>
|
|
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
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.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
|
|
PG would do it by default but since we override coq-prog-args it
doesn't.
|
|
|
|
This makes it so that
~~~ocaml
module M = struct
type a
let f (x:a) = x
end
type b = M.a
let _ = M.f 2
~~~
We get
Error: This expression has type int but an expression was expected of type M.a
instead of
Error: This expression has type int but an expression was expected of type b
We want this for Coq since we have numerous aliases in this pattern,
eg module_ident = Id.t in names.
See https://github.com/ocaml/dune/issues/1794 https://caml.inria.fr/mantis/view.php?id=7911
|
|
Note that `states` doesn't work reliably yet, but that is a separate
problem that will be fixed in Dune 1.6.
[Or we could also fix it improving the rules in envars.ml]
|
|
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: vbgl
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: gares
|
|
Closes coq/coq#9669
|
|
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.
|
|
Co-authored-by: Clément Pit-Claudel <clement.pitclaudel@live.com>
|
|
|
|
|
|
|
|
|
|
Deprecate the old syntax.
The documented syntax was using a with clause which is more standard with a hint database
than the using clause that was actually implemented.
|
