aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-10Bump version number to 8.10+alpha.Guillaume Melquiond
2018-09-07Merge PR #8437: Recover lost snippetThéo Zimmermann
2018-09-07Merge PR #8435: [dune] Fix build of coq_dune in 4.02.3Théo Zimmermann
2018-09-07Recover lost snippetMatěj G
This snippet on pattern matching got lost in the process of migrating to Sphynx.
2018-09-07Merge PR #8428: Add utop to default.nix for use in nix-shell (see #8426).Vincent Laporte
2018-09-07[dune] Fix build of coq_dune in 4.02.3Emilio Jesus Gallego Arias
Fixes #8431
2018-09-07Merge PR #8423: coqpp: allow DEPRECATED when declaring tacticsPierre-Marie Pédrot
2018-09-07Add utop to default.nix for use in nix-shell (see #8426).Théo Zimmermann
2018-09-07Merge PR #8426: [dune] [doc] Document `dune utop $lib`Théo Zimmermann
2018-09-07Merge PR #8411: Changes to default.nix to be able to use Dune.Vincent Laporte
2018-09-06Merge PR #8412: [dune] [ci] Fix and test release profile + use 1.1 ↵Gaëtan Gilbert
dune-workspace
2018-09-06[dune] [doc] Document `dune utop $lib`Emilio Jesus Gallego Arias
2018-09-06[dune] [ci] Fix and test release profile + use 1.1 dune-workspaceEmilio Jesus Gallego Arias
Dune 1.1 allows us to define the `env` flags in the workspace file, which is a better place than the current situation. Along the way, We fix the build flags for release mode [missing `-rectypes` and add a `release` build profile CI job.
2018-09-06Deprecation warning in legacy tacextend.mlpVincent Laporte
2018-09-06deprecation is CODE instead of IDENTVincent Laporte
2018-09-06coqpp: allow DEPRECATED when declaring tacticsVincent Laporte
2018-09-06Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate.Pierre-Marie Pédrot
2018-09-06Merge PR #8394: Print the entire string to the CoqIDE screen, e.g. for ↵Pierre-Marie Pédrot
"Print Options"
2018-09-06Merge PR #8415: [bin] Fix binary location procedure to work with symlinks.Pierre-Marie Pédrot
2018-09-06Merge PR #8420: [pfedit] Fix master build due to merge conflictGaëtan Gilbert
2018-09-06[pfedit] Fix master build due to merge conflictEmilio Jesus Gallego Arias
2018-09-06Merge PR #8302: Fix #7795: UGraph.AlreadyDeclared with ProgramMatthieu Sozeau
2018-09-06Override Dune derivation to update it before nixpkgs.Théo Zimmermann
As suggested by Vincent.
2018-09-06Changes to default.nix to be able to use Dune.Théo Zimmermann
2018-09-06Merge PR #8295: Fix #8291: print universe names in universe context for Check.Matthieu Sozeau
2018-09-05[bin] Fix binary location procedure to work with symlinks.Emilio Jesus Gallego Arias
In #7860 `Sys.executable_name` was introduced to locate coq private binaries; however, this breaks use cases with symlinks, such as Dune. In order to fix this, we adopt a simpler strategy; we will always adapt the name originally provided by the user, and only add a directory if it was originally present. This should work (hopefully) in all cases. This fixes `coqide` not working on Dune builds.
2018-09-05Merge PR #6857: [build] Preliminary support for building with `dune`.Théo Zimmermann
2018-09-05Merge PR #7968: Restrict universes in comInductiveGaëtan Gilbert
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
[Dune](https://github.com/ocaml/dune) is a compositional declarative build system for OCaml. It provides automatic generation of `version.ml`, `.merlin`, `META`, `opam`, API documentation; install management; easy integration with external libraries, test runners, and modular builds. In particular, Dune uniformly handles components regardless whether they live in, or out-of-tree. This greatly simplifies cases where a plugin [or CoqIde] is checked out in the current working copy but then distributed separately [and vice-versa]. Dune can thus be used as a more flexible `coq_makefile` replacement. For now we provide experimental support for a Dune build. In order to build Coq + the standard library with Dune type: ``` $ make -f Makefile.dune world ``` This PR includes a preliminary, developer-only preview of Dune for Coq. There is still ongoing work, see https://github.com/coq/coq/issues/8052 for tracking status towards full support. ## Technical description. Dune works out of the box with Coq, once we have fixed some modularity issues. The main remaining challenge was to support `.vo` files. As Dune doesn't support custom build rules yet, to properly build `.vo` files we provide a small helper script `tools/coq_dune.ml`. The script will scan the Coq library directories and generate the corresponding rules for `.v -> .vo` and `.ml4 -> .ml` builds. The script uses `coqdep` as to correctly output the dependencies of `.v` files. `coq_dune` is akin to `coq_makefile` and should be able to be used to build Coq projects in the future. Due to this pitfall, the build process has to proceed in three stages: 1) build `coqdep` and `coq_dune`; 2) generate `dune` files for `theories` and `plugins`; 3) perform a regular build with all targets are in scope. ## FAQ ### Why Dune? Coq has a moderately complex build system and it is not a secret that many developer-hours have been spent fighting with `make`. In particular, the current `make`-based system does offer poor support to verify that the current build rules and variables are coherent, and requires significant manual, error-prone. Many variables must be passed by hand, duplicated, etc... Additionally, our make system offers poor integration with now standard OCaml ecosystem tools such as `opam`, `ocamlfind` or `odoc`. Another critical point is build compositionality. Coq is rich in 3rd party contributions, and a big shortcoming of the current make system is that it cannot be used to build these projects; requiring us to maintain a custom tool, `coq_makefile`, with the corresponding cost. In the past, there has been some efforts to migrate Coq to more specialized build systems, however these stalled due to a variety of reasons. Dune, is a declarative, OCaml-specific build tool that is on the path to become the standard build system for the OCaml ecosystem. Dune seems to be a good fit for Coq well: it is well-supported, fast, compositional, and designed for large projects. ### Does Dune replace the make-based build system? The current, make-based build system is unmodified by this PR and kept as the default option. However, Dune has the potential ### Is this PR complete? What does it provide? This PR is ready for developer preview and feedback. The build system is functional, however, more work is necessary in order to make Dune the default for Coq. The main TODOs are tracked at https://github.com/coq/coq/issues/8052 This PR allows developers to use most of the features of Dune today: - Modular organization of the codebase; each component is built only against declared dependencies so components are checked for containment more strictly. - Hygienic builds; Dune places all artifacts under `_build`. - Automatic generation of `.install` files, simplified OPAM workflow. - `utop` support, `-opaque` in developer mode, etc... - `ml4` files are handled using `coqp5`, a native-code customized camlp5 executable which brings much faster `ml4 -> ml` processing. ### What dependencies does Dune require? Dune doesn't depend on any 3rd party package other than the OCaml compiler. ### Some Benchs: ``` $ /usr/bin/time make DUNEOPT="-j 1000" -f Makefile.dune states 59.50user 18.81system 0:29.83elapsed 262%CPU (0avgtext+0avgdata 302996maxresident)k 0inputs+646632outputs (0major+4893811minor)pagefaults 0swaps $ /usr/bin/time sh -c "./configure -local -native-compiler no && make -j states" 88.21user 23.65system 0:32.96elapsed 339%CPU (0avgtext+0avgdata 304992maxresident)k 0inputs+1051680outputs (0major+5300680minor)pagefaults 0swaps ```
2018-09-04[misc] Remove leftover files.Emilio Jesus Gallego Arias
Dune will complain about these leftovers / dead files in the tree.
2018-09-04Merge PR #7684: [doc] Build ML API documentation artifact.Gaëtan Gilbert
2018-09-04Merge PR #8263: Do not abstract over the named variable in unsafe ↵Hugo Herbelin
introduction tactic.
2018-09-04Merge PR #8264: More efficient computation of avoided variables during ↵Hugo Herbelin
pretyping.
2018-09-03Fix for issue #8378. If the string matches the regex, output theJim Fehrle
part before the regex match with full highlights. (Duh)
2018-09-03Merge PR #8387: Make -compat 8.8 import Coq.Compat.Coq88Théo Zimmermann
2018-09-03Merge PR #8064: Numeral notation (revisited again)Hugo Herbelin
2018-09-03[doc] Build ML API documentation artifact.Emilio Jesus Gallego Arias
This is not optimal for we have to rebuild the `.cmi` as `ocamldoc` cannot yet use the `_install_ci/` directory. Overall the `mli` documentation is in a sorry state, however, I think this is a first step in order to improve it. Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs investigation. cc: #7155
2018-09-03Merge PR #891: Check universes are declaredGaëtan Gilbert
2018-09-03Merge PR #8376: Source basic overlay after user overlays to fix #8375 ↵Gaëtan Gilbert
following #8348.
2018-09-03Merge PR #8124: Fix #8121: anomalies in native_compute with let and evars.Maxime Dénès
2018-09-03Merge PR #7953: More efficient abstraction over variables in Cooking.Maxime Dénès
2018-09-03Merge PR #7912: Simplify effects APIMaxime Dénès
2018-09-03Merge PR #7085: Turn the kernel reduction sharing flag into an argument ↵Maxime Dénès
passed in the cache
2018-09-03Merge PR #8147: [ssr] assertion -> error message (Fix #8134)Maxime Dénès
2018-09-03Merge PR #8359: [ssr] move ssr_*v tests to test-suite/ssr/Maxime Dénès
2018-09-02Merge PR #8363: Fix #8361: dependency states: camldevfilesJason Gross
2018-09-03Merge PR #8107: Fixes #8106: anomaly if declaring levels for only printing ↵Emilio Jesus Gallego Arias
then only parsing
2018-09-03Merge PR #8286: Fixing #7867: class error message tried to print a "fun" ↵Emilio Jesus Gallego Arias
with no binders
2018-09-02Make -compat 8.8 import Coq.Compat.Coq88Jason Gross
Fixes #8311
2018-09-02Fixing #7867 (class error message tries to print a "fun" with no binder).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:56:29 +0000