Skip to content
Branch: master
Find file History
ejgallego [dune] Move to Dune 1.10, use coq.pp directive.
We use the `(coq.pp ...)` dune directive which will produce correct
error messages for `.mlg` files.

Unfortunately we cannot yet use the automatic opam generation features
of Dune 1.10, as this does require a fully native Dune build.

Dune 1.6-1.10 has quite a few other improvements that could be used by
Coq, for example for promote modes.

I have fixed a couple of documentation issues. `Drop` and `ocamldebug`
have been tested in this version.
Latest commit 1c34e22 Jun 11, 2019
Permalink
Type Name Latest commit message Commit time
..
Failed to load latest commit information.
build [dune] Move to Dune 1.10, use coq.pp directive. Aug 22, 2019
ci [ci] Remove dead code. Aug 20, 2019
doc [dune] Move to Dune 1.10, use coq.pp directive. Aug 22, 2019
nsis Fixing typos - Part 1 May 21, 2019
shim Dune: do not use with-outputs-to for shims Jul 21, 2019
tools merge-pr.sh: filter reviews to remove the PR author Jul 9, 2019
v8-syntax Remove Show Script (deprecated in 8.10) May 31, 2019
Bugzilla_Coq_autolink.user.js autolink to Github PRs from Bugzilla Oct 3, 2017
Coq_Bugzilla_autolink.user.js Bugzilla autolink: avoid linking inside links (fix #5974). Oct 18, 2017
README.md Refactor and expand contributing guide. Jul 11, 2019
base_db [build] Refactoring to config lib and ocamldebug tweaks. Oct 22, 2018
base_include [error] Remove special error printing pre-processing Jul 6, 2019
bugzilla2github_stripped.csv Mention the migration from Bugzilla to GitHub issues in dev/doc/changes. Oct 27, 2017
core.dbg Fixing imports in debug printers: gramlib depends on Loc which is in … Dec 11, 2018
core_dune.dbg [ocamldebug] Fix load order after gramlib refactoring. Feb 11, 2019
db [build] Refactoring to config lib and ocamldebug tweaks. Oct 22, 2018
dune [dune] Support for coqide as an ocamldebug target. Jun 17, 2019
dune-dbg.in [dune] Support for coqide as an ocamldebug target. Jun 17, 2019
dune-workspace.all [core] [api] Support OCaml 4.08 Jul 8, 2019
dune_db [dune] Compile debug and checker printers. Oct 22, 2018
dynlink.ml Turn mltop.ml4 into a regular ocaml file Oct 6, 2012
header.c Update c-style headers to new year. Jun 17, 2019
header.ml Update ml-style headers to new year. Jun 17, 2019
header.py Update py-style headers to new year. Jun 17, 2019
inc_ltac [dev] Add include versions for Dune builds. Feb 18, 2019
inc_ltac_dune [dev] Add include versions for Dune builds. Feb 18, 2019
incdir [dev] Add include versions for Dune builds. Feb 18, 2019
incdir_dune [dune] Fix include object dirs. Apr 4, 2019
include [dev] Add include versions for Dune builds. Feb 18, 2019
include_dune [dev] Add include versions for Dune builds. Feb 18, 2019
include_printers Add aucontext debug printer May 14, 2019
lint-commits.sh CI: Test ml compilation of each commit in a PR in lint job Jun 6, 2019
lint-repository.sh Fix per-commit linting with bot merges Feb 18, 2019
macosify_accel.sh Coqide MacOS integration refresh Apr 27, 2012
nixpkgs.nix [dune] Move to Dune 1.10, use coq.pp directive. Aug 22, 2019
ocamldebug-coq.run Rename generated directory gramlib__pack -> gramlib/.pack Dec 6, 2018
top_printers.dbg Add aucontext debug printer May 14, 2019
top_printers.ml [api] Deprecate GlobRef constructors. Jul 8, 2019
top_printers.mli Update ml-style headers to new year. Jun 17, 2019
vm_printers.ml Add a non-cumulative impredicative universe SProp. Mar 14, 2019

README.md

This directory contains information and tools to help develop the Coq system

Debugging and profiling (dev/)

More info on debugging: dev/doc/debugging.md

File Description
dev/ocamldebug-coq To launch ocaml debugger (generated by the configure script)
dev/db To install pretty-printers from ocaml debugger
dev/base_db To install raw pretty-printers from ocaml debugger
dev/include To install pretty-printers from ocaml toplevel (use with the coq Drop command)
dev/base_include To install raw pretty-printers from ocaml toplevel
dev/vm_printers.ml, top_printers.ml ML pretty-printers for debugging

Miscellaneous information about the code (dev/doc)

Beginner's guide to hacking Coq: dev/doc/README.md

File Description
dev/doc/changes.md (partial) Per-version summary of the evolution of Coq ML source
dev/doc/style.txt A few style recommendations for writing Coq ML files
dev/doc/debugging.md Help for debugging or profiling
dev/doc/universes.txt Help for debugging universes
dev/doc/extensions.txt Some help about TACTIC EXTEND
dev/doc/perf-analysis Analysis of perfs measured on the compilation of user contribs
dev/doc/econstr.md Describes Econstr, implementation of treatment of evar in the engine
dev/doc/primproj.md Describes primitive projections
dev/doc/proof-engine.md Tutorial on new proof engine
dev/doc/xml-protocol.md XML protocol that coqtop and IDEs use to communicate
dev/doc/MERGING.md How pull requests should be merged into master
dev/doc/release-process.md Process of creating a new Coq release

Documentation of ML interfaces using odoc ( _build/default/_doc)

make -f Makefile.dune apidoc in coq root directory.

Other development tools (dev/tools)

File Description
dev/tools/coqdev.el Helper customizations for everyday Coq development, eg making compile work in subdirectories
dev/tools/objects.el Various development utilities at emacs level
You can’t perform that action at this time.