diff options
| -rw-r--r-- | .github/CODEOWNERS | 1 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 14 | ||||
| -rw-r--r-- | .ocamlinit | 1 | ||||
| -rw-r--r-- | Makefile.dune | 12 | ||||
| -rw-r--r-- | default.nix | 19 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 11 | ||||
| -rw-r--r-- | dune | 4 | ||||
| -rw-r--r-- | dune-project | 2 | ||||
| -rw-r--r-- | dune-workspace | 6 |
9 files changed, 54 insertions, 16 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 65c971ce76..274a0001b1 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -258,6 +258,7 @@ ########## Dune ########## +/.ocamlinit @ejgallego /Makefile.dune @ejgallego /tools/coq_dune* @ejgallego /dune* @ejgallego diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7f770feded..693a0b6bf0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -89,6 +89,7 @@ after_script: - set +e .dune-template: &dune-template + dependencies: [] stage: build artifacts: name: "$CI_JOB_NAME" @@ -97,9 +98,7 @@ after_script: expire_in: 1 week script: - set -e - - echo 'start:coq.dune' - - make -f Makefile.dune world - - echo 'end:coq.dune' + - make -f Makefile.dune "$DUNE_TARGET" - set +e # every non build job must set dependencies otherwise all build @@ -217,10 +216,11 @@ build:edge+flambda: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -flambda-opts " COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures" -build:egde:dune: +build:egde:dune:dev: <<: *dune-template variables: OPAM_SWITCH: edge + DUNE_TARGET: world windows64: <<: *windows-template @@ -234,6 +234,12 @@ windows32: except: - /^pr-.*$/ +pkg:dune-release: + <<: *dune-template + stage: test + variables: + OPAM_SWITCH: edge + DUNE_TARGET: release pkg:nix: image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git diff --git a/.ocamlinit b/.ocamlinit new file mode 100644 index 0000000000..3771334e12 --- /dev/null +++ b/.ocamlinit @@ -0,0 +1 @@ +#rectypes;; diff --git a/Makefile.dune b/Makefile.dune index 6056151c0d..f90f555557 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -10,10 +10,11 @@ BUILD_CONTEXT=_build/default help: @echo "Welcome to Coq's Dune-based build system. Targets are:" - @echo " - states: build a minimal functional coqtop" - @echo " - world: build all binaries and libraries" - @echo " - clean: remove build directory and autogenerated files" - @echo " - help: show this message" + @echo " - states: build a minimal functional coqtop" + @echo " - world: build all binaries and libraries" + @echo " - release: build Coq in release mode" + @echo " - clean: remove build directory and autogenerated files" + @echo " - help: show this message" voboot: dune build $(DUNEOPT) @vodeps @@ -25,6 +26,9 @@ states: voboot world: voboot dune build $(DUNEOPT) @install +release: voboot + dune build $(DUNEOPT) -p coq + clean: dune clean diff --git a/default.nix b/default.nix index d9317bccaf..35da15eebd 100644 --- a/default.nix +++ b/default.nix @@ -23,8 +23,8 @@ { pkgs ? (import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/060a98e9f4ad879492e48d63e887b0b6db26299e.tar.gz"; - sha256 = "1lzvp3md0hf6kp2bvc6dbzh40navlyd51qlns9wbkz6lqk3lgf6j"; + url = "https://github.com/NixOS/nixpkgs/archive/4477cf04b6779a537cdb5f0bd3dd30e75aeb4a3b.tar.gz"; + sha256 = "1i39wsfwkvj9yryj8di3jibpdg3b3j86ych7s9rb6z79k08yaaxc"; }) {}) , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06 , buildIde ? true @@ -38,6 +38,18 @@ with pkgs; with stdenv.lib; +let dune = + overrideDerivation jbuilder (o: { + name = "dune-1.1.1"; + src = fetchFromGitHub { + owner = "ocaml"; + repo = "dune"; + rev = "1.1.1"; + sha256 = "0v2pnxpmqsvrvidpwxvbsypzhqfdnjs5crjp9y61qi8nyj8d75zw"; + }; + }); +in + stdenv.mkDerivation rec { name = "coq"; @@ -45,6 +57,7 @@ stdenv.mkDerivation rec { buildInputs = [ hostname python2 time # coq-makefile timing tools + dune ] ++ (with ocamlPackages; [ ocaml findlib camlp5_strict num ]) ++ optional buildIde ocamlPackages.lablgtk @@ -71,7 +84,7 @@ stdenv.mkDerivation rec { else with builtins; filterSource (path: _: - !elem (baseNameOf path) [".git" "result" "bin" "_build_ci"]) ./.; + !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci"]) ./.; prefixKey = "-prefix "; diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 0b3e414513..85aaf317ef 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -39,6 +39,17 @@ In order to build a single package, you can do `dune build $PACKAGE.install`. Dune also provides targets for documentation and testing, see below. +## Developer shell + +You can create a developer shell with `dune utop $library`, where +`$library` can be any directory in the current workspace. For example, +`dune utop engine` or `dune utop plugins/ltac` will launch `utop` with +the right libraries already loaded. + +Note that you must invoke the `#rectypes;;` toplevel flag in order to +use Coq libraries. The provided `.ocamlinit` file does this +automatically. + ## Compositionality, developer and release modes. By default [in "developer mode"], Dune will compose all the packages @@ -9,7 +9,3 @@ (name vodeps) (deps tools/coq_dune.exe .vfiles.d)) ; (action (run coq_dune .vfiles.d)))) - -; Add custom flags here. Default developer profile is `dev` -(env - (dev (flags :standard -rectypes -w -9-27-50))) diff --git a/dune-project b/dune-project index b98bfa1013..6ce4ec4717 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +1,3 @@ -(lang dune 1.0) +(lang dune 1.1) (name coq-devel) diff --git a/dune-workspace b/dune-workspace new file mode 100644 index 0000000000..682631e7dc --- /dev/null +++ b/dune-workspace @@ -0,0 +1,6 @@ +(lang dune 1.1) + +; Add custom flags here. Default developer profile is `dev` +(env + (dev (flags :standard -rectypes -w -9-27-50)) + (release (flags :standard -rectypes))) |