aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.github/CODEOWNERS1
-rw-r--r--.gitlab-ci.yml14
-rw-r--r--.ocamlinit1
-rw-r--r--Makefile.dune12
-rw-r--r--coqpp/coqpp_ast.mli1
-rw-r--r--coqpp/coqpp_lex.mll1
-rw-r--r--coqpp/coqpp_main.ml11
-rw-r--r--coqpp/coqpp_parse.mly11
-rw-r--r--default.nix21
-rw-r--r--dev/doc/build-system.dune.md11
-rw-r--r--doc/sphinx/addendum/extended-pattern-matching.rst11
-rw-r--r--dune4
-rw-r--r--dune-project2
-rw-r--r--dune-workspace6
-rw-r--r--grammar/tacextend.mlp2
-rw-r--r--tools/coq_dune.ml30
16 files changed, 108 insertions, 31 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/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
index 39b4d2ab34..181c43615b 100644
--- a/coqpp/coqpp_ast.mli
+++ b/coqpp/coqpp_ast.mli
@@ -81,6 +81,7 @@ type grammar_ext = {
type tactic_ext = {
tacext_name : string;
tacext_level : int option;
+ tacext_deprecated : code option;
tacext_rules : tactic_rule list;
}
diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll
index 6c6562c204..bfa4e2b57b 100644
--- a/coqpp/coqpp_lex.mll
+++ b/coqpp/coqpp_lex.mll
@@ -95,6 +95,7 @@ rule extend = parse
| "END" { END }
| "DECLARE" { DECLARE }
| "PLUGIN" { PLUGIN }
+| "DEPRECATED" { DEPRECATED }
(** Camlp5 specific keywords *)
| "GLOBAL" { GLOBAL }
| "FIRST" { FIRST }
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 1648167a27..a8ed95f5ba 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -316,10 +316,17 @@ let print_rules fmt rules =
fprintf fmt "Tacentries.([@[<v>%a@]])" print_rules rules
let print_ast fmt ext =
+ let deprecation fmt =
+ function
+ | None -> ()
+ | Some { code } -> fprintf fmt "~deprecation:(%s) " code
+ in
let pr fmt () =
let level = match ext.tacext_level with None -> 0 | Some i -> i in
- fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a"
- plugin_name ext.tacext_name level print_rules ext.tacext_rules
+ fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a%a"
+ plugin_name ext.tacext_name level
+ deprecation ext.tacext_deprecated
+ print_rules ext.tacext_rules
in
let () = fprintf fmt "let () = @[%a@]\n" pr () in
()
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly
index baafd633c4..bf435fd247 100644
--- a/coqpp/coqpp_parse.mly
+++ b/coqpp/coqpp_parse.mly
@@ -62,7 +62,7 @@ let parse_user_entry s sep =
%token <string> IDENT QUALID
%token <string> STRING
%token <int> INT
-%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN
+%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED
%token LBRACKET RBRACKET PIPE ARROW COMMA EQUAL
%token LPAREN RPAREN COLON SEMICOLON
%token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA
@@ -108,8 +108,13 @@ vernac_extend:
;
tactic_extend:
-| TACTIC EXTEND IDENT tactic_level tactic_rules END
- { TacticExt { tacext_name = $3; tacext_level = $4; tacext_rules = $5 } }
+| TACTIC EXTEND IDENT tactic_deprecated tactic_level tactic_rules END
+ { TacticExt { tacext_name = $3; tacext_deprecated = $4; tacext_level = $5; tacext_rules = $6 } }
+;
+
+tactic_deprecated:
+| { None }
+| DEPRECATED CODE { Some $2 }
;
tactic_level:
diff --git a/default.nix b/default.nix
index d9317bccaf..80dca47f69 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
@@ -63,7 +76,7 @@ stdenv.mkDerivation rec {
)
++ optionals shell (
[ jq curl git gnupg ] # Dependencies of the merging script
- ++ (with ocamlPackages; [ merlin ocp-indent ocp-index ]) # Dev tools
+ ++ (with ocamlPackages; [ merlin ocp-indent ocp-index utop ]) # Dev tools
);
src =
@@ -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
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index f7fd4b9146..e507a224c6 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -407,12 +407,11 @@ length, by writing
.. coqtop:: in
- Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
- listn (n + m) :=
- match l in listn n, l' return listn (n + m) with
- | niln, x => x
- | consn n' a y, x => consn (n' + m) a (concat n' y m x)
- end.
+ Check (fun n (a b: listn n) =>
+ match a, b with
+ | niln, b0 => tt
+ | consn n' a y, bS => tt
+ end).
we have a copy of :g:`b` in type :g:`listn 0` resp. :g:`listn (S n')`.
diff --git a/dune b/dune
index 2a77d62a16..b758fc7b56 100644
--- a/dune
+++ b/dune
@@ -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)))
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 07239e7af0..5943600b7c 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -8,6 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+(** WARNING: this file is deprecated; consider modifying coqpp instead. *)
+
(** Implementation of the TACTIC EXTEND macro. *)
open Q_util
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index c89c78c8ec..ab60920fbc 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -80,6 +80,7 @@ module Aux = struct
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
(* Slower version of DirMap.update, waiting for OCaml 4.06.0 *)
@@ -103,6 +104,29 @@ module Aux = struct
end
done;
sub s 0 !j :: !r
+
+ (* Available in OCaml >= 4.04 *)
+ let is_dir_sep = match Sys.os_type with
+ | "Win32" -> fun s i -> s.[i] = '\\'
+ | _ -> fun s i -> s.[i] = '/'
+
+ let extension_len name =
+ let rec check i0 i =
+ if i < 0 || is_dir_sep name i then 0
+ else if name.[i] = '.' then check i0 (i - 1)
+ else String.length name - i0
+ in
+ let rec search_dot i =
+ if i < 0 || is_dir_sep name i then 0
+ else if name.[i] = '.' then check i (i - 1)
+ else search_dot (i - 1)
+ in
+ search_dot (String.length name - 1)
+
+ let remove_extension name =
+ let l = extension_len name in
+ if l = 0 then name else String.sub name 0 (String.length name - l)
+
end
let add_map_list key elem map =
@@ -181,18 +205,18 @@ let pp_vo_dep dir fmt vo =
(* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *)
let deps = List.map (fun s -> sdir ^ s) (edep @ vo.deps) in
(* The source file is also corrected as we will call coqtop from the top dir *)
- let source = String.concat "/" dir ^ "/" ^ Filename.(remove_extension vo.target) ^ ".v" in
+ let source = String.concat "/" dir ^ "/" ^ Legacy.(remove_extension vo.target) ^ ".v" in
(* The final build rule *)
let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s -compile %s))" eflag cflag source in
pp_rule fmt [vo.target] deps action
let pp_ml4_dep _dir fmt ml =
- let target = Filename.(remove_extension ml) ^ ".ml" in
+ let target = Legacy.(remove_extension ml) ^ ".ml" in
let ml4_rule = "(run coqp5 -loc loc -impl %{pp-file} -o %{targets})" in
pp_rule fmt [target] [ml] ml4_rule
let pp_mlg_dep _dir fmt ml =
- let target = Filename.(remove_extension ml) ^ ".ml" in
+ let target = Legacy.(remove_extension ml) ^ ".ml" in
let ml4_rule = "(run coqpp %{pp-file})" in
pp_rule fmt [target] [ml] ml4_rule
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 04:49:04 +0000