coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-30	dune: Don't echo "$(pwd)" when creating the shims	Gaëtan Gilbert
	AFAICT `echo "$(pwd)"` is unsound for the dune cache when called from different paths (typically different git worktrees).
2019-07-21	Dune: do not use with-outputs-to for shims	Gaëtan Gilbert
	We only want stdout, so if there's something in stderr it will both make a wrong output and make it harder to debug.
2019-03-28	[dune] Fix shim quoting and add coqc wrapper.	Emilio Jesus Gallego Arias
	The quoting was incorrect thus scripts didn't properly work.
2019-03-12	[dune] Add shim for coqtop.byte	Emilio Jesus Gallego Arias
	We add a shim for running the byte version of coqtop. This fixes the Coq part of #9727 , the Dune part is still open at https://github.com/ocaml/dune/issues/108 but this PR includes a workaround. Unfortunately we have to introduce a small inefficiency in the build process as we build both byte and native versions of plugins for this work reliable. As this is a choice done during bootstrap it won't be easy to fix until we have our own `dune coqtop` command and we can control the rules depending on the final target. This should affect the `check` target so still fast builds should be possible, but if this is a problem we could add a `byteboot` target to help.
2019-03-03	[dune] Shim for starting `coqtop/coqide` with minimal config.	Emilio Jesus Gallego Arias
	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.