| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
This is intended to be separate from handling of implicit binders.
The remaining uses of declare_manual_implicits satisfy a lot of
assertions, giving the possibility of simplifying the interface in the
future.
Two disabled warnings are added for things that currently pass silently.
Currently only Mtac passes non-maximal implicits to
declare_manual_implicits with the force-usage flag set. When implicit
arguments don't have to be named, should move Mtac over to
set_implicits.
|
|
Ack-by: JasonGross
Reviewed-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
See #9616
|
|
By default Coq warnings are made fatal when building the manual.
If you want to show a command resulting in a warning, use the warn
option.
Preexisting warnings are either fixed or marked as expected.
|
|
To be used when pushing an artifact to a github repository
|
|
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: rgrinberg
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
Ideally this will be handled by Dune's native library support, but
this could be useful for the likes of #9648.
I am not sure what should be done w.r.t. style files.
|
|
doesn't check enough
Ack-by: SkySkimmer
Reviewed-by: vbgl
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: vbgl
|
