aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml26
-rw-r--r--INSTALL.md4
-rw-r--r--azure-pipelines.yml2
-rw-r--r--configure.ml3
-rwxr-xr-xdev/ci/azure-opam.sh2
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile4
-rw-r--r--dev/dune-workspace.all4
-rw-r--r--doc/changelog/11-infrastructure-and-dependencies/11131-ci+back_to_ocaml_410.rst7
-rw-r--r--test-suite/output/PatternsInBinders.out5
-rw-r--r--vernac/comDefinition.ml42
-rw-r--r--vernac/g_vernac.mlg22
11 files changed, 89 insertions, 32 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index f2e0c362b4..caed21f5c3 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-19-V29"
+ CACHEKEY: "bionic_coq-V2020-03-27-V12"
IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
# By default, jobs run in the base switch; override to select another switch
OPAM_SWITCH: "base"
@@ -537,6 +537,30 @@ test-suite:edge:dune:dev:
# Gitlab doesn't support yet "expire_in: never" so we use the instance default
# expire_in: never
+test-suite:edge+4.11+trunk+dune:
+ stage: stage-1
+ dependencies: []
+ script:
+ - opam switch create 4.11.0 --empty
+ - eval $(opam env)
+ - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git
+ - opam update
+ - opam install ocaml-variants=4.11.0+trunk
+ - opam install dune num
+ - eval $(opam env)
+ - export COQ_UNIT_TEST=noop
+ - make -f Makefile.dune test-suite
+ variables:
+ OPAM_SWITCH: base
+ artifacts:
+ name: "$CI_JOB_NAME.logs"
+ when: always
+ paths:
+ - _build/log
+ - _build/default/test-suite/logs
+ expire_in: 2 week
+ allow_failure: true
+
test-suite:base+async:
extends: .test-suite-template
dependencies:
diff --git a/INSTALL.md b/INSTALL.md
index 0c98a611a5..2397f2c5c2 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -7,7 +7,7 @@ Build Requirements
To compile Coq yourself, you need:
- [OCaml](https://ocaml.org/) (version >= 4.05.0)
- (This version of Coq has been tested up to OCaml 4.09.1)
+ (This version of Coq has been tested up to OCaml 4.10.0)
- The [num](https://github.com/ocaml/num) library; note that it is
included in the OCaml distribution for OCaml versions < 4.06.0
@@ -45,7 +45,7 @@ CoqIDE with:
Opam (https://opam.ocaml.org/) is recommended to install OCaml and
the corresponding packages.
- $ opam switch create coq 4.09.1+flambda
+ $ opam switch create coq 4.10.0+flambda
$ eval $(opam env)
$ opam install num ocamlfind lablgtk3-sourceview3
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index aae2c3cb42..0bc30f0196 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -72,7 +72,7 @@ jobs:
opam list
displayName: 'Install OCaml dependencies'
env:
- COMPILER: "4.09.1"
+ COMPILER: "4.10.0"
FINDLIB_VER: ".1.8.1"
OPAMYES: "true"
diff --git a/configure.ml b/configure.ml
index ee2e50ef86..eaa0e321b0 100644
--- a/configure.ml
+++ b/configure.ml
@@ -616,8 +616,9 @@ let camltag = match caml_version_list with
45: "open" shadowing a label or constructor: see 44
48: implicit elimination of optional arguments: too common
58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9
+ 67: "unused functor parameter" seems totally bogus
*)
-let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-58"
+let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-58-67"
let coq_warn_error =
if !prefs.warn_error
then "-warn-error +a"
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 7b3e2703b8..64936cd236 100755
--- a/dev/ci/azure-opam.sh
+++ b/dev/ci/azure-opam.sh
@@ -2,7 +2,7 @@
set -e -x
-OPAM_VARIANT=ocaml-variants.4.09.1+mingw64c
+OPAM_VARIANT=ocaml-variants.4.10.0+mingw64c
wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz
tar -xf opam64.tar.xz
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index e56e4d38ea..0c8733c75a 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-03-19-V29"
+# CACHEKEY: "bionic_coq-V2020-03-27-V12"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -56,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
opam install $BASE_OPAM
# EDGE switch
-ENV COMPILER_EDGE="4.09.1" \
+ENV COMPILER_EDGE="4.10.0" \
BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0"
# EDGE+flambda switch, we install CI_OPAM as to be able to use
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index 556493ffad..d6348a3624 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -3,5 +3,5 @@
; Add custom flags here. Default developer profile is `dev`
(context (opam (switch 4.05.0)))
(context (opam (switch 4.05.0+32bit)))
-(context (opam (switch 4.09.1)))
-(context (opam (switch 4.09.1+flambda)))
+(context (opam (switch 4.10.0)))
+(context (opam (switch 4.10.0+flambda)))
diff --git a/doc/changelog/11-infrastructure-and-dependencies/11131-ci+back_to_ocaml_410.rst b/doc/changelog/11-infrastructure-and-dependencies/11131-ci+back_to_ocaml_410.rst
new file mode 100644
index 0000000000..778d37e07b
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/11131-ci+back_to_ocaml_410.rst
@@ -0,0 +1,7 @@
+- **Added:**
+ Bump official OCaml support and CI testing to 4.10.0
+ (`#11131 <https://github.com/coq/coq/pull/11131>`_,
+ `#11123 <https://github.com/coq/coq/pull/11123>`_,
+ `#11102 <https://github.com/coq/coq/pull/11123>`_,
+ by Emilio Jesus Gallego Arias, Jacques-Henri Jourdan,
+ Guillaume Melquiond, and Guillaume Munch-Maccagnoni).
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 4f09f00c56..bdfa8afb6a 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -4,7 +4,7 @@ fun '(x, y) => (y, x)
: A * B -> B * A
forall '(x, y), swap (x, y) = (y, x)
: Prop
-proj_informative = fun '(exist _ x _) => x : A
+proj_informative = fun '(exist _ x _) => x
: {x : A | P x} -> A
foo = fun '(Bar n b tt p) => if b then n + p else n - p
: Foo -> nat
@@ -29,8 +29,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w)
∀ '(x, y), swap (x, y) = (y, x)
: Prop
both_z =
-fun pat : nat * nat =>
-let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p)
+fun pat : nat * nat => let '(n, p) as x := pat return (F x) in (Z n, Z p)
: forall pat : nat * nat, F pat
fun '(x, y) '(z, t) => swap (x, y) = (z, t)
: A * B -> B * A -> Prop
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 3532d16315..8a91e9e63f 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -39,10 +39,50 @@ let check_imps ~impsty ~impsbody =
| [], [] -> () in
aux impsty impsbody
+let protect_pattern_in_binder bl c ctypopt =
+ (* We turn "Definition d binders := body : typ" into *)
+ (* "Definition d := fun binders => body:type" *)
+ (* This is a hack while waiting for LocalPattern in regular environments *)
+ if List.exists (function Constrexpr.CLocalPattern _ -> true | _ -> false) bl
+ then
+ let t = match ctypopt with
+ | None -> CAst.make ?loc:c.CAst.loc (Constrexpr.CHole (None,Namegen.IntroAnonymous,None))
+ | Some t -> t in
+ let loc = Loc.merge_opt c.CAst.loc t.CAst.loc in
+ let c = CAst.make ?loc @@ Constrexpr.CCast (c, Glob_term.CastConv t) in
+ let loc = match List.hd bl with
+ | Constrexpr.CLocalAssum (a::_,_,_) | Constrexpr.CLocalDef (a,_,_) -> a.CAst.loc
+ | Constrexpr.CLocalPattern {CAst.loc} -> loc
+ | Constrexpr.CLocalAssum ([],_,_) -> assert false in
+ let apply_under_binders f env evd c =
+ let rec aux env evd c =
+ let open Constr in
+ let open EConstr in
+ let open Context.Rel.Declaration in
+ match kind evd c with
+ | Lambda (x,t,c) ->
+ let evd,c = aux (push_rel (LocalAssum (x,t)) env) evd c in
+ evd, mkLambda (x,t,c)
+ | LetIn (x,b,t,c) ->
+ let evd,c = aux (push_rel (LocalDef (x,b,t)) env) evd c in
+ evd, mkLetIn (x,t,b,c)
+ | Case (ci,p,a,bl) ->
+ let evd,bl = Array.fold_left_map (aux env) evd bl in
+ evd, mkCase (ci,p,a,bl)
+ | Cast (c,_,_) -> f env evd c (* we remove the cast we had set *)
+ (* This last case may happen when reaching the proof of an
+ impossible case, as when pattern-matching on a vector of length 1 *)
+ | _ -> (evd,c) in
+ aux env evd c in
+ ([], Constrexpr_ops.mkLambdaCN ?loc:(Loc.merge_opt loc c.CAst.loc) bl c, None, apply_under_binders)
+ else
+ (bl, c, ctypopt, fun f env evd c -> f env evd c)
+
let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
let env = Global.env() in
(* Explicitly bound universes and constraints *)
let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
+ let (bl, c, ctypopt, apply_under_binders) = protect_pattern_in_binder bl c ctypopt in
(* Build the parameters *)
let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in
(* Build the type *)
@@ -62,7 +102,7 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
evd, c, imps1@impsty, Some ty
in
(* Do the reduction *)
- let evd, c = red_constant_body red_option env_bl evd c in
+ let evd, c = apply_under_binders (red_constant_body red_option) env_bl evd c in
(* Declare the definition *)
let c = EConstr.it_mkLambda_or_LetIn c ctx in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index a8f1a49086..a1cdc718d7 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -348,25 +348,11 @@ GRAMMAR EXTEND Gram
(* Simple definitions *)
def_body:
[ [ bl = binders; ":="; red = reduce; c = lconstr ->
- { if List.exists (function CLocalPattern _ -> true | _ -> false) bl
- then
- (* FIXME: "red" will be applied to types in bl and Cast with remain *)
- let c = mkLambdaCN ~loc bl c in
- DefineBody ([], red, c, None)
- else
- (match c with
- | { CAst.v = CCast(c, CastConv t) } -> DefineBody (bl, red, c, Some t)
- | _ -> DefineBody (bl, red, c, None)) }
+ { match c.CAst.v with
+ | CCast(c, Glob_term.CastConv t) -> DefineBody (bl, red, c, Some t)
+ | _ -> DefineBody (bl, red, c, None) }
| bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
- { let ((bl, c), tyo) =
- if List.exists (function CLocalPattern _ -> true | _ -> false) bl
- then
- (* FIXME: "red" will be applied to types in bl and Cast with remain *)
- let c = CAst.make ~loc @@ CCast (c, CastConv t) in
- (([],mkLambdaCN ~loc bl c), None)
- else ((bl, c), Some t)
- in
- DefineBody (bl, red, c, tyo) }
+ { DefineBody (bl, red, c, Some t) }
| bl = binders; ":"; t = lconstr ->
{ ProveBody (bl, t) } ] ]
;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 18:54:40 +0000