From bc411fa4d8c04424c579d506dd0507cb83db7bc7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 9 Apr 2020 23:09:39 -0400 Subject: [ci] [build] Bump Dune to 2.5.0 It is unfortunate that we cannot install coqide and Dune 2.5.0 in < 4.07.0 --- .gitlab-ci.yml | 2 +- coq.opam | 2 +- dev/ci/docker/bionic_coq/Dockerfile | 6 +++--- dev/nixpkgs.nix | 4 ++-- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index acbec54695..f1dc793ee7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-03-27-V12" + CACHEKEY: "bionic_coq-V2020-03-11-V28" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/coq.opam b/coq.opam index 39191c21d9..aa19c2cf98 100644 --- a/coq.opam +++ b/coq.opam @@ -22,7 +22,7 @@ version: "dev" depends: [ "ocaml" { >= "4.05.0" } - "dune" { >= "2.0.0" } + "dune" { >= "2.5.0" } "ocamlfind" { build } "num" ] diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 0c8733c75a..58677b8496 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-03-27-V12" +# CACHEKEY: "bionic_coq-V2020-03-11-V28" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,7 +37,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.1 ounit.2.2.2 odoc.1.5.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.1 ounit.2.2.2 odoc.1.5.0" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ BASE_ONLY_OPAM="elpi.1.10.2" @@ -57,7 +57,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ # EDGE switch ENV COMPILER_EDGE="4.10.0" \ - BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0" + BASE_OPAM_EDGE="dune.2.5.0 dune-release.1.3.3 ocamlformat.0.13.0" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index b8a696ef21..fb84155392 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/34e41a91547e342f6fbc901929134b34000297eb.tar.gz"; - sha256 = "0mlqxim36xg8aj4r35mpcgqg27wy1dbbim9l1cpjl24hcy96v48w"; + url = "https://github.com/NixOS/nixpkgs/archive/807ca93fadd5197c2260490de0c76e500562dc05.tar.gz"; + sha256 = "10yq8bnls77fh3pk5chkkb1sv5lbdgyk1rr2v9xn71rr1k2x563p"; }) -- cgit v1.2.3 From 5db591257070734439dd5550995d6d3f497256c0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 22 Mar 2019 06:33:49 +0100 Subject: [dune] [stdlib] Build the standard library natively with Dune. This completes a pure Dune bootstrap of Coq. There is still the question if we should modify `coqdep` so it does output a dependency on `Init.Prelude.vo` in certain cases. TODO: We still double-add `theories` and `plugins` [in coqinit and in Dune], this should be easy to clean up. Setting `libs_init_load_path` does give a correct build indeed; however we still must call this for compatibility? --- .gitignore | 5 - Makefile.dune | 73 ++++----- coq.opam | 1 - dev/doc/build-system.dune.md | 7 +- dune | 21 +-- dune-project | 7 +- plugins/btauto/dune | 7 + plugins/btauto/plugin_base.dune | 5 - plugins/cc/dune | 7 + plugins/cc/plugin_base.dune | 5 - plugins/derive/dune | 7 + plugins/derive/plugin_base.dune | 5 - plugins/extraction/dune | 7 + plugins/extraction/plugin_base.dune | 5 - plugins/firstorder/dune | 7 + plugins/firstorder/plugin_base.dune | 5 - plugins/funind/dune | 7 + plugins/funind/plugin_base.dune | 5 - plugins/ltac/dune | 15 ++ plugins/ltac/plugin_base.dune | 13 -- plugins/micromega/dune | 24 +++ plugins/micromega/plugin_base.dune | 22 --- plugins/nsatz/dune | 7 + plugins/nsatz/plugin_base.dune | 5 - plugins/omega/dune | 7 + plugins/omega/plugin_base.dune | 5 - plugins/rtauto/dune | 7 + plugins/rtauto/plugin_base.dune | 5 - plugins/setoid_ring/dune | 7 + plugins/setoid_ring/plugin_base.dune | 5 - plugins/ssr/dune | 9 ++ plugins/ssr/plugin_base.dune | 7 - plugins/ssrmatching/dune | 7 + plugins/ssrmatching/plugin_base.dune | 5 - plugins/syntax/dune | 36 +++++ plugins/syntax/plugin_base.dune | 34 ---- theories/dune | 38 +++++ tools/coq_dune.ml | 301 ----------------------------------- tools/dune | 6 +- user-contrib/Ltac2/dune | 14 ++ 40 files changed, 258 insertions(+), 507 deletions(-) create mode 100644 plugins/btauto/dune delete mode 100644 plugins/btauto/plugin_base.dune create mode 100644 plugins/cc/dune delete mode 100644 plugins/cc/plugin_base.dune create mode 100644 plugins/derive/dune delete mode 100644 plugins/derive/plugin_base.dune create mode 100644 plugins/extraction/dune delete mode 100644 plugins/extraction/plugin_base.dune create mode 100644 plugins/firstorder/dune delete mode 100644 plugins/firstorder/plugin_base.dune create mode 100644 plugins/funind/dune delete mode 100644 plugins/funind/plugin_base.dune create mode 100644 plugins/ltac/dune delete mode 100644 plugins/ltac/plugin_base.dune create mode 100644 plugins/micromega/dune delete mode 100644 plugins/micromega/plugin_base.dune create mode 100644 plugins/nsatz/dune delete mode 100644 plugins/nsatz/plugin_base.dune create mode 100644 plugins/omega/dune delete mode 100644 plugins/omega/plugin_base.dune create mode 100644 plugins/rtauto/dune delete mode 100644 plugins/rtauto/plugin_base.dune create mode 100644 plugins/setoid_ring/dune delete mode 100644 plugins/setoid_ring/plugin_base.dune create mode 100644 plugins/ssr/dune delete mode 100644 plugins/ssr/plugin_base.dune create mode 100644 plugins/ssrmatching/dune delete mode 100644 plugins/ssrmatching/plugin_base.dune create mode 100644 plugins/syntax/dune delete mode 100644 plugins/syntax/plugin_base.dune create mode 100644 theories/dune delete mode 100644 tools/coq_dune.ml create mode 100644 user-contrib/Ltac2/dune diff --git a/.gitignore b/.gitignore index b665b2f86d..adbf9dd189 100644 --- a/.gitignore +++ b/.gitignore @@ -184,11 +184,6 @@ plugins/ssr/ssrvernac.ml META.coq # Files automatically generated by Dune. -plugins/*/dune -theories/*/dune -theories/*/*/dune -theories/*/*/*/dune -/user-contrib/Ltac2/dune *.install !Makefile.install diff --git a/Makefile.dune b/Makefile.dune index b77e78db69..efdea2ab85 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -1,27 +1,27 @@ # -*- mode: makefile -*- # Dune Makefile for Coq -.PHONY: help voboot states world watch check # Main developer targets +.PHONY: help states world watch check # Main developer targets .PHONY: coq coqide coqide-server # Package targets .PHONY: quickbyte quickopt quickide # Partial / quick developer targets .PHONY: refman-html refman-pdf stdlib-html apidoc # Documentation targets -.PHONY: test-suite release # Accessory targets +.PHONY: test-suite release install # Accessory targets .PHONY: fmt ocheck ireport clean # Maintenance targets +.PHONY: voboot # Added just not to break old scripts # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short -BOOT_DIR=_build_boot -BOOT_CONTEXT=$(BOOT_DIR)/default - help: - @echo "Welcome to Coq's Dune-based build system. Targets are:" + @echo "Welcome to Coq's Dune-based build system. Common targets are:" @echo "" @echo " - states: build a minimal functional coqtop" - @echo " - world: build all binaries and libraries" - @echo " - watch: build all binaries and libraries [continuous build]" + @echo " - world: build all public binaries and libraries" + @echo " - watch: build all public binaries and libraries [continuous build]" @echo " - check: build all ML files as fast as possible" @echo "" + @echo " Targets to build Coq in developer mode:" + @echo "" @echo " - coq: build package Coq [toplevel compilers, tools, stdlib, no GTK]" @echo " - coqide-server: build package coqide-server [XML protocol language server]" @echo " - coqide: build package CoqIDE [gtk application]" @@ -35,43 +35,41 @@ help: @echo " - refman-pdf: build Coq's reference manual [PDF version]" @echo " - stdlib-html: build Coq's Stdlib documentation [HTML version]" @echo " - apidoc: build ML API documentation" - @echo " - release: build Coq in release mode" @echo "" @echo " - fmt: run ocamlformat on the codebase" @echo " - ocheck: build for all supported OCaml versions [requires OPAM]" @echo " - ireport: build with optimized flambda settings and emit an inline report" @echo " - clean: remove build directory and autogenerated files" @echo " - help: show this message" + @echo "" + @echo " To build Coq in release mode, use 'dune build -p package'." + @echo " To install Coq in release mode, use 'dune install -p package'." + @echo " See Dune documentation for more information." -# We need to bootstrap with a dummy coq.plugins.ltac so install targets do work. -plugins/ltac/dune: - @echo "(library (name ltac_plugin) (public_name coq.plugins.ltac) (modules_without_implementation extraargs extratactics))" > plugins/ltac/dune - -voboot: plugins/ltac/dune - dune build --build-dir=$(BOOT_DIR) $(DUNEOPT) @vodeps - dune exec --build-dir=$(BOOT_DIR) -- ./tools/coq_dune.exe $(BOOT_CONTEXT)/.vfiles.d +voboot: + @echo "This target is empty and not needed anymore" -states: voboot +states: dune build --display=short $(DUNEOPT) dev/shim/coqtop-prelude NONDOC_INSTALL_TARGETS:=coq.install coqide-server.install coqide.install -world: voboot +world: dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -coq: voboot +coq: dune build $(DUNEOPT) coq.install -coqide: voboot +coqide: dune build $(DUNEOPT) coqide.install -coqide-server: voboot +coqide-server: dune build $(DUNEOPT) coqide-server.install -watch: voboot +watch: dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -w -check: voboot +check: dune build $(DUNEOPT) @check COQTOP_FILES=ide/idetop.bc ide/coqide_main.bc checker/coqchk.bc @@ -80,43 +78,46 @@ PRINTER_FILES=dev/top_printers.cma QUICKBYTE_TARGETS=$(COQTOP_FILES) $(PLUGIN_FILES:.mlpack=.cma) $(PRINTER_FILES) topbin/coqtop_byte_bin.bc QUICKOPT_TARGETS=$(COQTOP_FILES:.bc=.exe) $(PLUGIN_FILES:.mlpack=.cmxs) $(PRINTER_FILES:.cma=.cmxa) topbin/coqtop_bin.exe -quickbyte: voboot +quickbyte: dune build $(DUNEOPT) $(QUICKBYTE_TARGETS) -quickopt: voboot +quickopt: dune build $(DUNEOPT) $(QUICKOPT_TARGETS) -quickide: states +quickide: dune build $(DUNEOPT) dev/shim/coqide-prelude -test-suite: voboot +test-suite: dune runtest --no-buffer $(DUNEOPT) -refman-html: voboot +refman-html: dune build @refman-html -refman-pdf: voboot +refman-pdf: dune build @refman-pdf -stdlib-html: voboot +stdlib-html: dune build @stdlib-html -apidoc: voboot +apidoc: dune build $(DUNEOPT) @doc -release: voboot +release: dune build $(DUNEOPT) -p coq -fmt: voboot +# We define this target as to override Make's built-in one +install: + @echo "To install Coq using dune, use 'dune install -p PACKAGE' where" + @echo "PACKAGE is any of the packages defined by opam files in the root dira" + +fmt: dune build @fmt --auto-promote -ocheck: voboot +ocheck: dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all ireport: dune clean - dune build --build-dir=$(BOOT_DIR) $(DUNEOPT) @vodeps - dune exec --build-dir=$(BOOT_DIR) -- ./tools/coq_dune.exe $(BOOT_CONTEXT)/.vfiles.d dune build $(DUNEOPT) @install --profile=ireport clean: diff --git a/coq.opam b/coq.opam index aa19c2cf98..e46f9def60 100644 --- a/coq.opam +++ b/coq.opam @@ -29,6 +29,5 @@ depends: [ build: [ [ "./configure" "-prefix" prefix ] - [ "make" "-f" "Makefile.dune" "voboot" ] [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 0506216541..8b0bf216e3 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -18,10 +18,6 @@ Dune will get confused if it finds leftovers of in-tree compilation, so please be sure your tree is clean from objects files generated by the make-based system. -If you want to build the standard libraries and plugins you should -call `make -f Makefile.dune voboot`. It is usually enough to do that -once per-session. - More helper targets are available in `Makefile.dune`, `make -f Makefile.dune` will display some help. @@ -55,7 +51,6 @@ Instead, you should use the provided "shims" for running `coqtop` and `coqide` in a fast build. In order to use them, do: ``` -$ make -f Makefile.dune voboot # Only once per session $ dune exec -- dev/shim/coqtop-prelude ``` @@ -153,7 +148,7 @@ depending on your OCaml version. This is due to several factors: ## Dropping from coqtop: -After doing `make -f Makefile.dune voboot`, the following commands should work: +The following commands should work: ``` dune exec -- dev/shim/coqbyte-prelude > Drop. diff --git a/dune b/dune index d59346ed68..cf7221ce62 100644 --- a/dune +++ b/dune @@ -18,29 +18,10 @@ ; ; (_ (flags :standard -rectypes))) -; Rules for coq_dune -(rule - (targets .vfiles.d) - (deps - (source_tree theories) - (source_tree plugins) - (source_tree user-contrib)) - (action - (with-stdout-to .vfiles.d - (bash "%{bin:coqdep} -dyndep both -noglob -boot -R theories Coq -Q user-contrib/Ltac2 Ltac2 -I user-contrib/Ltac2 \ - `find plugins/ -maxdepth 1 -mindepth 1 -type d -printf '-I %p '` \ - `find theories user-contrib -type f -name *.v`")))) - -(alias - (name vodeps) - (deps tools/coq_dune.exe .vfiles.d)) - ; (action (run coq_dune .vfiles.d)))) - (install (section lib) (package coq) - (files - revision)) + (files revision)) (rule (targets revision) diff --git a/dune-project b/dune-project index fa05f5fb41..873d03e8dd 100644 --- a/dune-project +++ b/dune-project @@ -1,11 +1,10 @@ -(lang dune 2.0) +(lang dune 2.5) (name coq) -(using coq 0.1) +(using coq 0.2) (formatting (enabled_for ocaml)) -; We cannot set this to true until as long as the build is not -; properly bootstrapped [that is, we remove the voboot target] +; TODO ; ; (generate_opam_files true) diff --git a/plugins/btauto/dune b/plugins/btauto/dune new file mode 100644 index 0000000000..d2f5b65980 --- /dev/null +++ b/plugins/btauto/dune @@ -0,0 +1,7 @@ +(library + (name btauto_plugin) + (public_name coq.plugins.btauto) + (synopsis "Coq's btauto plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_btauto)) diff --git a/plugins/btauto/plugin_base.dune b/plugins/btauto/plugin_base.dune deleted file mode 100644 index 6a024358c3..0000000000 --- a/plugins/btauto/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name btauto_plugin) - (public_name coq.plugins.btauto) - (synopsis "Coq's btauto plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/cc/dune b/plugins/cc/dune new file mode 100644 index 0000000000..f7fa3adb56 --- /dev/null +++ b/plugins/cc/dune @@ -0,0 +1,7 @@ +(library + (name cc_plugin) + (public_name coq.plugins.cc) + (synopsis "Coq's congruence closure plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_congruence)) diff --git a/plugins/cc/plugin_base.dune b/plugins/cc/plugin_base.dune deleted file mode 100644 index 2a92996d2a..0000000000 --- a/plugins/cc/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name cc_plugin) - (public_name coq.plugins.cc) - (synopsis "Coq's congruence closure plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/derive/dune b/plugins/derive/dune new file mode 100644 index 0000000000..1931339471 --- /dev/null +++ b/plugins/derive/dune @@ -0,0 +1,7 @@ +(library + (name derive_plugin) + (public_name coq.plugins.derive) + (synopsis "Coq's derive plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_derive)) diff --git a/plugins/derive/plugin_base.dune b/plugins/derive/plugin_base.dune deleted file mode 100644 index ba9cd595ce..0000000000 --- a/plugins/derive/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name derive_plugin) - (public_name coq.plugins.derive) - (synopsis "Coq's derive plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/extraction/dune b/plugins/extraction/dune new file mode 100644 index 0000000000..0c01dcd488 --- /dev/null +++ b/plugins/extraction/dune @@ -0,0 +1,7 @@ +(library + (name extraction_plugin) + (public_name coq.plugins.extraction) + (synopsis "Coq's extraction plugin") + (libraries num coq.plugins.ltac)) + +(coq.pp (modules g_extraction)) diff --git a/plugins/extraction/plugin_base.dune b/plugins/extraction/plugin_base.dune deleted file mode 100644 index 037b0d5053..0000000000 --- a/plugins/extraction/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name extraction_plugin) - (public_name coq.plugins.extraction) - (synopsis "Coq's extraction plugin") - (libraries num coq.plugins.ltac)) diff --git a/plugins/firstorder/dune b/plugins/firstorder/dune new file mode 100644 index 0000000000..1b05452d8f --- /dev/null +++ b/plugins/firstorder/dune @@ -0,0 +1,7 @@ +(library + (name ground_plugin) + (public_name coq.plugins.firstorder) + (synopsis "Coq's first order logic solver plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_ground)) diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/plugin_base.dune deleted file mode 100644 index d88daa23fc..0000000000 --- a/plugins/firstorder/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name ground_plugin) - (public_name coq.plugins.firstorder) - (synopsis "Coq's first order logic solver plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/funind/dune b/plugins/funind/dune new file mode 100644 index 0000000000..e594ffbd02 --- /dev/null +++ b/plugins/funind/dune @@ -0,0 +1,7 @@ +(library + (name recdef_plugin) + (public_name coq.plugins.funind) + (synopsis "Coq's functional induction plugin") + (libraries coq.plugins.extraction)) + +(coq.pp (modules g_indfun)) diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune deleted file mode 100644 index 6ccf15df29..0000000000 --- a/plugins/funind/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name recdef_plugin) - (public_name coq.plugins.funind) - (synopsis "Coq's functional induction plugin") - (libraries coq.plugins.extraction)) diff --git a/plugins/ltac/dune b/plugins/ltac/dune new file mode 100644 index 0000000000..6558ecbfe8 --- /dev/null +++ b/plugins/ltac/dune @@ -0,0 +1,15 @@ +(library + (name ltac_plugin) + (public_name coq.plugins.ltac) + (synopsis "Coq's LTAC tactic language") + (modules :standard \ tauto) + (libraries coq.stm)) + +(library + (name tauto_plugin) + (public_name coq.plugins.tauto) + (synopsis "Coq's tauto tactic") + (modules tauto) + (libraries coq.plugins.ltac)) + +(coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs)) diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune deleted file mode 100644 index 5611f5ba16..0000000000 --- a/plugins/ltac/plugin_base.dune +++ /dev/null @@ -1,13 +0,0 @@ -(library - (name ltac_plugin) - (public_name coq.plugins.ltac) - (synopsis "Coq's LTAC tactic language") - (modules :standard \ tauto) - (libraries coq.stm)) - -(library - (name tauto_plugin) - (public_name coq.plugins.tauto) - (synopsis "Coq's tauto tactic") - (modules tauto) - (libraries coq.plugins.ltac)) diff --git a/plugins/micromega/dune b/plugins/micromega/dune new file mode 100644 index 0000000000..33ad3a0138 --- /dev/null +++ b/plugins/micromega/dune @@ -0,0 +1,24 @@ +(library + (name micromega_plugin) + (public_name coq.plugins.micromega) + ; be careful not to link the executable to the plugin! + (modules (:standard \ csdpcert g_zify zify)) + (synopsis "Coq's micromega plugin") + (libraries num coq.plugins.ltac)) + +(executable + (name csdpcert) + (public_name csdpcert) + (package coq) + (modules csdpcert) + (flags :standard -open Micromega_plugin) + (libraries coq.plugins.micromega)) + +(library + (name zify_plugin) + (public_name coq.plugins.zify) + (modules g_zify zify) + (synopsis "Coq's zify plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_micromega g_zify)) diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/plugin_base.dune deleted file mode 100644 index 4153d06161..0000000000 --- a/plugins/micromega/plugin_base.dune +++ /dev/null @@ -1,22 +0,0 @@ -(library - (name micromega_plugin) - (public_name coq.plugins.micromega) - ; be careful not to link the executable to the plugin! - (modules (:standard \ csdpcert g_zify zify)) - (synopsis "Coq's micromega plugin") - (libraries num coq.plugins.ltac)) - -(executable - (name csdpcert) - (public_name csdpcert) - (package coq) - (modules csdpcert) - (flags :standard -open Micromega_plugin) - (libraries coq.plugins.micromega)) - -(library - (name zify_plugin) - (public_name coq.plugins.zify) - (modules g_zify zify) - (synopsis "Coq's zify plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/nsatz/dune b/plugins/nsatz/dune new file mode 100644 index 0000000000..b921c9c408 --- /dev/null +++ b/plugins/nsatz/dune @@ -0,0 +1,7 @@ +(library + (name nsatz_plugin) + (public_name coq.plugins.nsatz) + (synopsis "Coq's nsatz solver plugin") + (libraries num coq.plugins.ltac)) + +(coq.pp (modules g_nsatz)) diff --git a/plugins/nsatz/plugin_base.dune b/plugins/nsatz/plugin_base.dune deleted file mode 100644 index 9da5b39972..0000000000 --- a/plugins/nsatz/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name nsatz_plugin) - (public_name coq.plugins.nsatz) - (synopsis "Coq's nsatz solver plugin") - (libraries num coq.plugins.ltac)) diff --git a/plugins/omega/dune b/plugins/omega/dune new file mode 100644 index 0000000000..0db71ed6fb --- /dev/null +++ b/plugins/omega/dune @@ -0,0 +1,7 @@ +(library + (name omega_plugin) + (public_name coq.plugins.omega) + (synopsis "Coq's omega plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_omega)) diff --git a/plugins/omega/plugin_base.dune b/plugins/omega/plugin_base.dune deleted file mode 100644 index f512501c78..0000000000 --- a/plugins/omega/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name omega_plugin) - (public_name coq.plugins.omega) - (synopsis "Coq's omega plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/rtauto/dune b/plugins/rtauto/dune new file mode 100644 index 0000000000..43efa0eca5 --- /dev/null +++ b/plugins/rtauto/dune @@ -0,0 +1,7 @@ +(library + (name rtauto_plugin) + (public_name coq.plugins.rtauto) + (synopsis "Coq's rtauto plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_rtauto)) diff --git a/plugins/rtauto/plugin_base.dune b/plugins/rtauto/plugin_base.dune deleted file mode 100644 index 233845ae0f..0000000000 --- a/plugins/rtauto/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name rtauto_plugin) - (public_name coq.plugins.rtauto) - (synopsis "Coq's rtauto plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/setoid_ring/dune b/plugins/setoid_ring/dune new file mode 100644 index 0000000000..60522cd3f5 --- /dev/null +++ b/plugins/setoid_ring/dune @@ -0,0 +1,7 @@ +(library + (name newring_plugin) + (public_name coq.plugins.setoid_ring) + (synopsis "Coq's setoid ring plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_newring)) diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/plugin_base.dune deleted file mode 100644 index d83857edad..0000000000 --- a/plugins/setoid_ring/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name newring_plugin) - (public_name coq.plugins.setoid_ring) - (synopsis "Coq's setoid ring plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/ssr/dune b/plugins/ssr/dune new file mode 100644 index 0000000000..a117d09a16 --- /dev/null +++ b/plugins/ssr/dune @@ -0,0 +1,9 @@ +(library + (name ssreflect_plugin) + (public_name coq.plugins.ssreflect) + (synopsis "Coq's ssreflect plugin") + (modules_without_implementation ssrast) + (flags :standard -open Gramlib) + (libraries coq.plugins.ssrmatching)) + +(coq.pp (modules ssrvernac ssrparser)) diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/plugin_base.dune deleted file mode 100644 index a13524bb52..0000000000 --- a/plugins/ssr/plugin_base.dune +++ /dev/null @@ -1,7 +0,0 @@ -(library - (name ssreflect_plugin) - (public_name coq.plugins.ssreflect) - (synopsis "Coq's ssreflect plugin") - (modules_without_implementation ssrast) - (flags :standard -open Gramlib) - (libraries coq.plugins.ssrmatching)) diff --git a/plugins/ssrmatching/dune b/plugins/ssrmatching/dune new file mode 100644 index 0000000000..629d723816 --- /dev/null +++ b/plugins/ssrmatching/dune @@ -0,0 +1,7 @@ +(library + (name ssrmatching_plugin) + (public_name coq.plugins.ssrmatching) + (synopsis "Coq ssrmatching plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_ssrmatching)) diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/plugin_base.dune deleted file mode 100644 index 06f67c3774..0000000000 --- a/plugins/ssrmatching/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name ssrmatching_plugin) - (public_name coq.plugins.ssrmatching) - (synopsis "Coq ssrmatching plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/syntax/dune b/plugins/syntax/dune new file mode 100644 index 0000000000..b395695c8a --- /dev/null +++ b/plugins/syntax/dune @@ -0,0 +1,36 @@ +(library + (name numeral_notation_plugin) + (public_name coq.plugins.numeral_notation) + (synopsis "Coq numeral notation plugin") + (modules g_numeral numeral) + (libraries coq.vernac)) + +(library + (name string_notation_plugin) + (public_name coq.plugins.string_notation) + (synopsis "Coq string notation plugin") + (modules g_string string_notation) + (libraries coq.vernac)) + +(library + (name r_syntax_plugin) + (public_name coq.plugins.r_syntax) + (synopsis "Coq syntax plugin: reals") + (modules r_syntax) + (libraries coq.vernac)) + +(library + (name int63_syntax_plugin) + (public_name coq.plugins.int63_syntax) + (synopsis "Coq syntax plugin: int63") + (modules int63_syntax) + (libraries coq.vernac)) + +(library + (name float_syntax_plugin) + (public_name coq.plugins.float_syntax) + (synopsis "Coq syntax plugin: float") + (modules float_syntax) + (libraries coq.vernac)) + +(coq.pp (modules g_numeral g_string)) diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune deleted file mode 100644 index 512752135d..0000000000 --- a/plugins/syntax/plugin_base.dune +++ /dev/null @@ -1,34 +0,0 @@ -(library - (name numeral_notation_plugin) - (public_name coq.plugins.numeral_notation) - (synopsis "Coq numeral notation plugin") - (modules g_numeral numeral) - (libraries coq.vernac)) - -(library - (name string_notation_plugin) - (public_name coq.plugins.string_notation) - (synopsis "Coq string notation plugin") - (modules g_string string_notation) - (libraries coq.vernac)) - -(library - (name r_syntax_plugin) - (public_name coq.plugins.r_syntax) - (synopsis "Coq syntax plugin: reals") - (modules r_syntax) - (libraries coq.vernac)) - -(library - (name int63_syntax_plugin) - (public_name coq.plugins.int63_syntax) - (synopsis "Coq syntax plugin: int63") - (modules int63_syntax) - (libraries coq.vernac)) - -(library - (name float_syntax_plugin) - (public_name coq.plugins.float_syntax) - (synopsis "Coq syntax plugin: float") - (modules float_syntax) - (libraries coq.vernac)) diff --git a/theories/dune b/theories/dune new file mode 100644 index 0000000000..b9af76d699 --- /dev/null +++ b/theories/dune @@ -0,0 +1,38 @@ +(coq.theory + (name Coq) + (package coq) + (synopsis "Coq's Standard Library") + (flags -q) + ; (mode native) + (boot) + ; (per_file + ; (Init/*.v -> -boot)) + (libraries + coq.plugins.ltac + coq.plugins.tauto + + coq.plugins.cc + coq.plugins.firstorder + + coq.plugins.numeral_notation + coq.plugins.string_notation + coq.plugins.int63_syntax + coq.plugins.r_syntax + coq.plugins.float_syntax + + coq.plugins.btauto + coq.plugins.rtauto + + coq.plugins.setoid_ring + coq.plugins.nsatz + coq.plugins.omega + + coq.plugins.zify + coq.plugins.micromega + + coq.plugins.funind + + coq.plugins.ssreflect + coq.plugins.derive)) + +(include_subdirs qualified) diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml deleted file mode 100644 index 472e6b4948..0000000000 --- a/tools/coq_dune.ml +++ /dev/null @@ -1,301 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* f x - | None -> () - - let option_cata d f o = match o with - | Some x -> f x - | None -> d - - let list_compare f = let rec lc x y = match x, y with - | [], [] -> 0 - | [], _ -> -1 - | _, [] -> 1 - | x::xs, y::ys -> let r = f x y in if r = 0 then lc xs ys else r - in lc - - let rec pp_list pp sep fmt l = match l with - | [] -> () - | [l] -> fprintf fmt "%a" pp l - | x::xs -> fprintf fmt "%a%a%a" pp x sep () (pp_list pp sep) xs - - let rec pmap f l = match l with - | [] -> [] - | x :: xs -> - begin match f x with - | None -> pmap f xs - | Some r -> r :: pmap f xs - end - - let sep fmt () = fprintf fmt "@;" - - (* Creation of paths, aware of the platform separator. *) - let bpath l = String.concat Filename.dir_sep l - - module DirOrd = struct - type t = string list - let compare = list_compare String.compare - end - - module DirMap = Map.Make(DirOrd) - - (* Functions available in newer OCaml versions *) - (* Taken from the OCaml std library (c) INRIA / LGPL-2.1 *) - module Legacy = struct - - - (* Fix once we move to OCaml >= 4.06.0 *) - let list_init len f = - let rec init_aux i n f = - if i >= n then [] - else let r = f i in r :: init_aux (i+1) n f - in init_aux 0 len f - - (* Slower version of DirMap.update, waiting for OCaml 4.06.0 *) - let dirmap_update key f map = - match begin - try f (Some (DirMap.find key map)) - with Not_found -> f None - end with - | None -> DirMap.remove key map - | Some x -> DirMap.add key x map - - end - - let add_map_list key elem map = - (* Move to Dirmap.update once we require OCaml >= 4.06.0 *) - Legacy.dirmap_update key (fun l -> Some (option_cata [elem] (fun ll -> elem :: ll) l)) map - - let replace_ext ~file ~newext = - Filename.(remove_extension file) ^ newext - -end - -open Aux - -(* Once this is a Dune plugin the flags will be taken from the env *) -module Options = struct - - type flag = { - enabled : bool; - cmd : string; - } - - let all_opts = - [ { enabled = false; cmd = "-debug"; } - ; { enabled = false; cmd = "-native_compiler"; } - ; { enabled = true; cmd = "-w +default"; } - ] - - let build_coq_flags () = - let popt o = if o.enabled then Some o.cmd else None in - String.concat " " @@ pmap popt all_opts -end - -type vodep = { - target: string; - deps : string list; -} - -type ldep = | VO of vodep | MLG of string -type ddir = ldep list DirMap.t - -(* Filter `.vio` etc... *) -let filter_no_vo = - List.filter (fun f -> Filename.check_suffix f ".vo") - -(* We could have coqdep to output dune files directly *) - -let gen_sub n = - (* Move to List.init once we can depend on OCaml >= 4.06.0 *) - bpath @@ Legacy.list_init n (fun _ -> "..") - -let pp_rule fmt targets deps action = - (* Special printing of the first rule *) - let ppl = pp_list pp_print_string sep in - let pp_deps fmt l = match l with - | [] -> - () - | x :: xs -> - fprintf fmt "(:pp-file %s)%a" x sep (); - pp_list pp_print_string sep fmt xs - in - fprintf fmt - "@[(rule@\n @[(targets @[%a@])@\n(deps @[%a@])@\n(action @[%a@])@])@]@\n" - ppl targets pp_deps deps pp_print_string action - -let gen_coqc_targets vo = - [ vo.target - ; replace_ext ~file:vo.target ~newext:".glob" - ; replace_ext ~file:vo.target ~newext:".vos" - ; "." ^ replace_ext ~file:vo.target ~newext:".aux"] - -(* Generate the dune rule: *) -let pp_vo_dep dir fmt vo = - let depth = List.length dir in - let sdir = gen_sub depth in - (* All files except those in Init implicitly depend on the Prelude, we account for it here. *) - let eflag, edep = if List.tl dir = ["Init"] then "-noinit -R theories Coq", [] else "", [bpath ["theories";"Init";"Prelude.vo"]] in - (* Coq flags *) - let cflag = Options.build_coq_flags () in - (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *) - let deps = List.map (fun s -> bpath [sdir;s]) (edep @ vo.deps) in - (* The source file is also corrected as we will call coqtop from the top dir *) - let source = bpath (dir @ [replace_ext ~file:vo.target ~newext:".v"]) in - (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *) - let libflag = "-coqlib %{project_root}" in - (* The final build rule *) - let action = sprintf "(chdir %%{project_root} (run coqc -q %s %s %s %s))" libflag eflag cflag source in - let all_targets = gen_coqc_targets vo in - pp_rule fmt all_targets deps action - -let pp_mlg_dep _dir fmt ml = - fprintf fmt "@[(coq.pp (modules %s))@]@\n" (Filename.remove_extension ml) - -let pp_dep dir fmt oo = match oo with - | VO vo -> pp_vo_dep dir fmt vo - | MLG f -> pp_mlg_dep dir fmt f - -let out_install fmt dir ff = - let itarget = String.concat "/" dir in - let ff = List.concat @@ pmap (function | VO vo -> Some (gen_coqc_targets vo) | _ -> None) ff in - let pp_ispec fmt tg = fprintf fmt "(%s as coq/%s)" tg (bpath [itarget;tg]) in - fprintf fmt "(install@\n @[(section lib_root)@\n(package coq)@\n(files @[%a@])@])@\n" - (pp_list pp_ispec sep) ff - -(* For each directory, we must record two things, the build rules and - the install specification. *) -let record_dune d ff = - let sd = bpath d in - if Sys.file_exists sd && Sys.is_directory sd then - let out = open_out (bpath [sd;"dune"]) in - let fmt = formatter_of_out_channel out in - if Sys.file_exists (bpath [sd; "plugin_base.dune"]) then - fprintf fmt "(include plugin_base.dune)@\n"; - out_install fmt d ff; - List.iter (pp_dep d fmt) ff; - fprintf fmt "%!"; - close_out out - else - eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd - -(* File Scanning *) -let scan_mlg ~root m d = - let dir = [root; d] in - let m = DirMap.add dir [] m in - let mlg = Sys.(List.filter (fun f -> Filename.(check_suffix f ".mlg")) - Array.(to_list @@ readdir (bpath dir))) in - List.fold_left (fun m f -> add_map_list [root; d] (MLG f) m) m mlg - -let scan_dir ~root m = - let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in - let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath [root;f]) Array.(to_list @@ readdir root)) in - List.fold_left (scan_mlg ~root) m dirs - -let scan_plugins m = scan_dir ~root:"plugins" m -let scan_usercontrib m = scan_dir ~root:"user-contrib" m - -(* This will be removed when we drop support for Make *) -let fix_cmo_cma file = - if String.equal Filename.(extension file) ".cmo" - then replace_ext ~file ~newext:".cma" - else file - -(* Process .vfiles.d and generate a skeleton for the dune file *) -let parse_coqdep_line l = - match Str.(split (regexp ":") l) with - | [targets;deps] -> - let targets = Str.(split (regexp "[ \t]+") targets) in - let deps = Str.(split (regexp "[ \t]+") deps) in - let targets = filter_no_vo targets in - begin match targets with - | [target] -> - let dir, target = Filename.(dirname target, basename target) in - (* coqdep outputs with the '/' directory separator regardless of - the platform. Anyways, I hope we can link to coqdep instead - of having to parse its output soon, that should solve this - kind of issues *) - let deps = List.map fix_cmo_cma deps in - Some (String.split_on_char '/' dir, VO { target; deps; }) - (* Otherwise a vio file, we ignore *) - | _ -> None - end - (* Strange rule, we ignore *) - | _ -> None - -let rec read_vfiles ic map = - try - let rule = parse_coqdep_line (input_line ic) in - (* Add vo_entry to its corresponding map entry *) - let map = option_cata map (fun (dir, vo) -> add_map_list dir vo map) rule in - read_vfiles ic map - with End_of_file -> map - -let out_map map = - DirMap.iter record_dune map - -let exec_ifile f = - match Array.length Sys.argv with - | 1 -> f stdin - | 2 -> - let in_file = Sys.argv.(1) in - begin try - let ic = open_in in_file in - (try f ic - with exn -> - eprintf "Error: exec_ifile @[%s@]@\n%!" (Printexc.to_string exn); - close_in ic) - with _ -> - eprintf "Error: cannot open input file %s@\n%!" in_file - end - | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1 - -let _ = - exec_ifile (fun ic -> - let map = scan_plugins DirMap.empty in - let map = scan_usercontrib map in - let map = read_vfiles ic map in - out_map map) diff --git a/tools/dune b/tools/dune index c0e4e20f72..d591bb0c37 100644 --- a/tools/dune +++ b/tools/dune @@ -49,8 +49,8 @@ (ocamllex coqwc) (executables - (names coq_tex coq_dune) - (public_names coq-tex coq_dune) + (names coq_tex) + (public_names coq-tex) (package coq) - (modules coq_tex coq_dune) + (modules coq_tex) (libraries str)) diff --git a/user-contrib/Ltac2/dune b/user-contrib/Ltac2/dune new file mode 100644 index 0000000000..90869a46a0 --- /dev/null +++ b/user-contrib/Ltac2/dune @@ -0,0 +1,14 @@ +(coq.theory + (name Ltac2) + (package coq) + (synopsis "Ltac2 tactic language") + (libraries coq.plugins.ltac2)) + +(library + (name ltac2_plugin) + (public_name coq.plugins.ltac2) + (synopsis "Ltac2 plugin") + (modules_without_implementation tac2expr tac2qexpr tac2types) + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_ltac2)) -- cgit v1.2.3 From 29aa2b5533a36e170fb0ed947f86e70d5b1cb8fb Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 18:34:09 -0400 Subject: [dune] [doc] Remove the quick targets in favor of the shims. These targets are redundant with the shims. We also improve the documentation quite a bit. --- Makefile.dune | 66 +++++++++++++++++++++++------------------------------------ 1 file changed, 26 insertions(+), 40 deletions(-) diff --git a/Makefile.dune b/Makefile.dune index efdea2ab85..9e1747a4c3 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -2,48 +2,57 @@ # Dune Makefile for Coq .PHONY: help states world watch check # Main developer targets -.PHONY: coq coqide coqide-server # Package targets -.PHONY: quickbyte quickopt quickide # Partial / quick developer targets .PHONY: refman-html refman-pdf stdlib-html apidoc # Documentation targets -.PHONY: test-suite release install # Accessory targets +.PHONY: test-suite .PHONY: fmt ocheck ireport clean # Maintenance targets -.PHONY: voboot # Added just not to break old scripts +.PHONY: voboot release install # Added just not to break old scripts # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short help: - @echo "Welcome to Coq's Dune-based build system. Common targets are:" + @echo "Welcome to Coq's Dune-based build system. Common developer targets are:" @echo "" @echo " - states: build a minimal functional coqtop" @echo " - world: build all public binaries and libraries" @echo " - watch: build all public binaries and libraries [continuous build]" @echo " - check: build all ML files as fast as possible" + @echo " - test-suite: run Coq's test suite" @echo "" - @echo " Targets to build Coq in developer mode:" + @echo " Note: these targets produce a developer build," + @echo " not suitable for distribution to end-users" @echo "" - @echo " - coq: build package Coq [toplevel compilers, tools, stdlib, no GTK]" - @echo " - coqide-server: build package coqide-server [XML protocol language server]" - @echo " - coqide: build package CoqIDE [gtk application]" + @echo " Documentation targets:" @echo "" - @echo " - quickbyte: build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler" - @echo " - quickopt: build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler" - @echo " - quickide: build main IDE files [client + server + prelude] using the optimizing compiler" - @echo "" - @echo " - test-suite: run Coq's test suite" @echo " - refman-html: build Coq's reference manual [HTML version]" @echo " - refman-pdf: build Coq's reference manual [PDF version]" @echo " - stdlib-html: build Coq's Stdlib documentation [HTML version]" @echo " - apidoc: build ML API documentation" @echo "" + @echo " Miscellaneous targets:" + @echo "" @echo " - fmt: run ocamlformat on the codebase" @echo " - ocheck: build for all supported OCaml versions [requires OPAM]" @echo " - ireport: build with optimized flambda settings and emit an inline report" @echo " - clean: remove build directory and autogenerated files" @echo " - help: show this message" @echo "" - @echo " To build Coq in release mode, use 'dune build -p package'." - @echo " To install Coq in release mode, use 'dune install -p package'." + @echo " To run an app \\in {coqc,coqtop,coqbyte,coqide}:" + @echo "" + @echo " - use 'dune exec -- dev/shim/app-prelude args'" + @echo "" + @echo " Provided opam/dune packages are:" + @echo "" + @echo " - coq: base Coq package, toplevel compilers, tools, stdlib, no GTK" + @echo " - coqide-server: XML protocol language server" + @echo " - coqide: CoqIDE gtk application" + @echo "" + @echo " To build a package, you can use:" + @echo "" + @echo " - 'dune build package.install' : build package in developer mode" + @echo " - 'dune build -p package' : build package in release mode" + @echo "" + @echo " Packages _must_ be installed using release mode, use: 'dune install -p package'" @echo " See Dune documentation for more information." voboot: @@ -57,36 +66,12 @@ NONDOC_INSTALL_TARGETS:=coq.install coqide-server.install coqide.install world: dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -coq: - dune build $(DUNEOPT) coq.install - -coqide: - dune build $(DUNEOPT) coqide.install - -coqide-server: - dune build $(DUNEOPT) coqide-server.install - watch: dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -w check: dune build $(DUNEOPT) @check -COQTOP_FILES=ide/idetop.bc ide/coqide_main.bc checker/coqchk.bc -PLUGIN_FILES=$(wildcard plugins/*/*.mlpack) -PRINTER_FILES=dev/top_printers.cma -QUICKBYTE_TARGETS=$(COQTOP_FILES) $(PLUGIN_FILES:.mlpack=.cma) $(PRINTER_FILES) topbin/coqtop_byte_bin.bc -QUICKOPT_TARGETS=$(COQTOP_FILES:.bc=.exe) $(PLUGIN_FILES:.mlpack=.cmxs) $(PRINTER_FILES:.cma=.cmxa) topbin/coqtop_bin.exe - -quickbyte: - dune build $(DUNEOPT) $(QUICKBYTE_TARGETS) - -quickopt: - dune build $(DUNEOPT) $(QUICKOPT_TARGETS) - -quickide: - dune build $(DUNEOPT) dev/shim/coqide-prelude - test-suite: dune runtest --no-buffer $(DUNEOPT) @@ -103,6 +88,7 @@ apidoc: dune build $(DUNEOPT) @doc release: + @echo "release target is deprecated, use dune directly" dune build $(DUNEOPT) -p coq # We define this target as to override Make's built-in one -- cgit v1.2.3