diff options
| -rw-r--r-- | .github/CODEOWNERS | 36 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 14 | ||||
| -rw-r--r-- | .ocamlinit | 1 | ||||
| -rw-r--r-- | Makefile.dune | 12 | ||||
| -rw-r--r-- | coqpp/coqpp_ast.mli | 1 | ||||
| -rw-r--r-- | coqpp/coqpp_lex.mll | 1 | ||||
| -rw-r--r-- | coqpp/coqpp_main.ml | 11 | ||||
| -rw-r--r-- | coqpp/coqpp_parse.mly | 11 | ||||
| -rw-r--r-- | default.nix | 21 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 11 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 11 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 6 | ||||
| -rw-r--r-- | dune | 4 | ||||
| -rw-r--r-- | dune-project | 2 | ||||
| -rw-r--r-- | dune-workspace | 6 | ||||
| -rw-r--r-- | grammar/tacextend.mlp | 2 | ||||
| -rw-r--r-- | pretyping/classops.ml | 28 | ||||
| -rw-r--r-- | pretyping/classops.mli | 2 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 9 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 30 |
20 files changed, 160 insertions, 59 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 65c971ce76..d9136ee24b 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -6,11 +6,23 @@ /.github/ @maximedenes # Secondary maintainer @Zimmi48 +########## Build system ########## + +/Makefile* @gares + +/configure* @ejgallego + +/META.coq.in @ejgallego + +/dev/build/windows @MSoegtropIMC +# Secondary maintainer @maximedenes + ########## CI infrastructure ########## /dev/ci/ @coq/ci-maintainers /.travis.yml @coq/ci-maintainers /.gitlab-ci.yml @coq/ci-maintainers +/Makefile.ci @coq/ci-maintainers /dev/ci/user-overlays/*.sh @ghost # Trick to avoid getting review requests @@ -21,8 +33,7 @@ /dev/ci/*.bat @maximedenes # Secondary maintainer @SkySkimmer -/default.nix @Zimmi48 -# Secondary maintainer @vbgl +*.nix @coq/nix-maintainers ########## Documentation ########## @@ -43,6 +54,7 @@ # each time someone modifies the dev changelog /doc/ @coq/doc-maintainers +/Makefile.doc @coq/doc-maintainers /man/ @silene # Secondary maintainer @maximedenes @@ -258,6 +270,7 @@ ########## Dune ########## +/.ocamlinit @ejgallego /Makefile.dune @ejgallego /tools/coq_dune* @ejgallego /dune* @ejgallego @@ -301,25 +314,6 @@ /vernac/ @mattam82 # Secondary maintainer @maximedenes -########## Build system ########## - -/Makefile* @gares - -/configure* @ejgallego - -/META.coq.in @ejgallego - -/dev/build/windows @MSoegtropIMC -# Secondary maintainer @maximedenes - -# This file belongs to CI -/Makefile.ci @ejgallego -# Secondary maintainer @SkySkimmer - -# This file belongs to the doc -/Makefile.doc @maximedenes -# Secondary maintainer @silene - ########## Test suite ########## /test-suite/Makefile @gares 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/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index c0c4539564..23cbd76eda 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -325,6 +325,12 @@ Coercions and Modules This option makes it possible to recover the behavior of the versions of |Coq| prior to 8.3. +.. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it. + + This warning is emitted when typechecking relies on a coercion + contained in a module that has not been explicitely imported. It helps + migrating code and stop relying on the option above. + Examples -------- @@ -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/pretyping/classops.ml b/pretyping/classops.ml index 542fb5456c..52e02c87fd 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -118,6 +118,9 @@ let class_tab = let coercion_tab = ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t) +let coercions_in_scope = + ref Refset_env.empty + module ClPairOrd = struct type t = cl_index * cl_index @@ -131,12 +134,13 @@ module ClPairMap = Map.Make(ClPairOrd) let inheritance_graph = ref (ClPairMap.empty : inheritance_path ClPairMap.t) -let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph) +let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph, !coercions_in_scope) -let unfreeze (fcl,fco,fig) = +let unfreeze (fcl,fco,fig,in_scope) = class_tab:=fcl; coercion_tab:=fco; - inheritance_graph:=fig + inheritance_graph:=fig; + coercions_in_scope:=in_scope (* ajout de nouveaux "objets" *) @@ -445,9 +449,16 @@ let load_coercion _ o = if !automatically_import_coercions then cache_coercion (Global.env ()) Evd.empty o +let set_coercion_in_scope (_, c) = + let r = c.coercion_type in + coercions_in_scope := Refset_env.add r !coercions_in_scope + let open_coercion i o = - if Int.equal i 1 && not !automatically_import_coercions then - cache_coercion (Global.env ()) Evd.empty o + if Int.equal i 1 then begin + set_coercion_in_scope o; + if not !automatically_import_coercions then + cache_coercion (Global.env ()) Evd.empty o + end let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in @@ -492,7 +503,9 @@ let inCoercion : coercion -> obj = open_function = open_coercion; load_function = load_coercion; cache_function = (fun objn -> - let env = Global.env () in cache_coercion env Evd.empty objn + let env = Global.env () in + set_coercion_in_scope objn; + cache_coercion env Evd.empty objn ); subst_function = subst_coercion; classify_function = classify_coercion; @@ -553,3 +566,6 @@ let hide_coercion coe = let coe_info = coercion_info coe in Some coe_info.coe_param else None + +let is_coercion_in_scope r = + Refset_env.mem r !coercions_in_scope diff --git a/pretyping/classops.mli b/pretyping/classops.mli index af00c0a8dc..dc193c4e74 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -113,3 +113,5 @@ val coercions : unit -> coe_info_typ list (** [hide_coercion] returns the number of params to skip if the coercion must be hidden, [None] otherwise; it raises [Not_found] if not a coercion *) val hide_coercion : coe_typ -> int option + +val is_coercion_in_scope : GlobRef.t -> bool diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 5e3821edf1..e15c00f7dc 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -363,12 +363,20 @@ let saturate_evd env evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd +let warn_coercion_not_in_scope = + CWarnings.create ~name:"coercion-not-in-scope" ~category:"deprecated" + Pp.(fun r -> str "Coercion used but not in scope: " ++ + Nametab.pr_global_env Id.Set.empty r ++ str ". If you want to use " + ++ str "this coercion, please Import the module that contains it.") + (* Apply coercion path from p to hj; raise NoCoercion if not applicable *) let apply_coercion env sigma p hj typ_cl = try let j,t,evd = List.fold_left (fun (ja,typ_cl,sigma) i -> + if not (is_coercion_in_scope i.coe_value) then + warn_coercion_not_in_scope i.coe_value; let isid = i.coe_is_identity in let isproj = i.coe_is_projection in let sigma, c = new_global sigma i.coe_value in @@ -386,7 +394,6 @@ let apply_coercion env sigma p hj typ_cl = (hj,typ_cl,sigma) p in evd, j with NoCoercion as e -> raise e - | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.") (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = 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 |