aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml6
-rw-r--r--Makefile.build4
-rw-r--r--Makefile.ci4
-rw-r--r--coqide-server.opam16
-rw-r--r--coqide.opam (renamed from ide/coqide.opam)1
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh2
-rwxr-xr-xdev/ci/ci-aac-tactics.sh8
-rwxr-xr-xdev/ci/ci-basic-overlay.sh6
-rw-r--r--dune7
-rw-r--r--dune-workspace6
-rw-r--r--ide/dune39
-rw-r--r--ide/dune-project3
-rw-r--r--ide/dune-workspace6
-rw-r--r--ide/fake_ide.ml (renamed from tools/fake_ide.ml)8
-rw-r--r--ide/protocol/dune2
-rw-r--r--interp/notation_ops.ml8
-rw-r--r--kernel/cClosure.ml10
-rw-r--r--kernel/cClosure.mli1
-rw-r--r--kernel/reduction.ml2
-rw-r--r--pretyping/inferCumulativity.ml2
-rw-r--r--test-suite/bugs/closed/8672.v5
21 files changed, 93 insertions, 53 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 118482273d..948e4f0a37 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -241,7 +241,8 @@ pkg:opam:
script:
- set -e
- opam pin add coq .
- - opam pin add coqide ide
+ - opam pin add coqide-server .
+ - opam pin add coqide .
- set +e
variables:
OPAM_SWITCH: edge
@@ -346,6 +347,9 @@ validate:edge+flambda:
OPAM_SWITCH: edge
OPAM_VARIANT: "+flambda"
+ci-aac-tactics:
+ <<: *ci-template
+
ci-bedrock2:
<<: *ci-template
diff --git a/Makefile.build b/Makefile.build
index 0faa18b059..ee758fcc5f 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -563,7 +563,7 @@ $(COQWORKMGRBYTE): $(COQWORKMGRCMO)
# fake_ide : for debugging or test-suite purpose, a fake ide simulating
# a connection to coqidetop
-FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo tools/fake_ide.cmo
+FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo ide/fake_ide.cmo
$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP)
$(SHOW)'OCAMLBEST -o $@'
@@ -668,7 +668,7 @@ kernel/kernel.cmxa: kernel/kernel.mllib
$(SHOW)'OCAMLOPT -pack -o $@'
$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
-COND_IDEFLAGS=$(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,)
+COND_IDEFLAGS=$(if $(filter ide/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,)
COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,)
COND_BYTEFLAGS= \
diff --git a/Makefile.ci b/Makefile.ci
index fb4f275e9e..8234da0869 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -8,7 +8,9 @@
## # (see LICENSE file for the text of the license) ##
##########################################################################
-CI_TARGETS=ci-bedrock2 \
+CI_TARGETS= \
+ ci-aac-tactics \
+ ci-bedrock2 \
ci-bignums \
ci-color \
ci-compcert \
diff --git a/coqide-server.opam b/coqide-server.opam
new file mode 100644
index 0000000000..546ce75dbd
--- /dev/null
+++ b/coqide-server.opam
@@ -0,0 +1,16 @@
+opam-version: "1.2"
+maintainer: "The Coq development team <coqdev@inria.fr>"
+authors: "The Coq development team, INRIA, CNRS, and contributors."
+homepage: "https://coq.inria.fr/"
+bug-reports: "https://github.com/coq/coq/issues"
+dev-repo: "https://github.com/coq/coq.git"
+license: "LGPL-2.1"
+
+available: [ocaml-version >= "4.05.0"]
+
+depends: [
+ "dune" { build & >= "1.2.0" }
+ "coq"
+]
+
+build: [ [ "dune" "build" "-p" name "-j" jobs ] ]
diff --git a/ide/coqide.opam b/coqide.opam
index 897177b283..17fb5dbbe2 100644
--- a/ide/coqide.opam
+++ b/coqide.opam
@@ -11,6 +11,7 @@ available: [ocaml-version >= "4.05.0"]
depends: [
"dune" { build & >= "1.2.0" }
"coq"
+ "coqide-server"
"conf-gtksourceview"
"lablgtk" { >= "2.18.5" }
]
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index b8bea755e0..c3d895784e 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1851,7 +1851,7 @@ function make_addon_coquelicot {
function make_addon_aactactics {
installer_addon_dependency aac
- if build_prep_overlay aactactis; then
+ if build_prep_overlay aactactics; then
installer_addon_section aac "AAC" "Coq plugin for extensible associative and commutative rewriting" ""
log1 make
log2 make install
diff --git a/dev/ci/ci-aac-tactics.sh b/dev/ci/ci-aac-tactics.sh
new file mode 100755
index 0000000000..896a0ddf66
--- /dev/null
+++ b/dev/ci/ci-aac-tactics.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download aactactics
+
+( cd "${CI_BUILD_DIR}/aactactics" && make && make install )
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 511eaaba9c..50d4d21637 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -252,6 +252,6 @@
########################################################################
# aac-tactics
########################################################################
-: "${aactactis_CI_REF:=master}"
-: "${aactactis_CI_GITURL:=https://github.com/coq-community/aac-tactics}"
-: "${aactactis_CI_ARCHIVEURL:=${aactactis_CI_GITURL}/archive}"
+: "${aactactics_CI_REF:=master}"
+: "${aactactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}"
+: "${aactactics_CI_ARCHIVEURL:=${aactactics_CI_GITURL}/archive}"
diff --git a/dune b/dune
index 27c5e972fe..b3073493ea 100644
--- a/dune
+++ b/dune
@@ -1,3 +1,9 @@
+; Default flags for all Coq libraries.
+(env
+ (dev (flags :standard -rectypes -w -9-27-50+60))
+ (release (flags :standard -rectypes)))
+
+; Rules for coq_dune
(rule
(targets .vfiles.d)
(deps
@@ -12,6 +18,7 @@
(install
(section lib)
+ (package coq)
(files
revision))
diff --git a/dune-workspace b/dune-workspace
deleted file mode 100644
index 38875eac2c..0000000000
--- a/dune-workspace
+++ /dev/null
@@ -1,6 +0,0 @@
-(lang dune 1.2)
-
-; Add custom flags here. Default developer profile is `dev`
-(env
- (dev (flags :standard -rectypes -w -9-27-50+60))
- (release (flags :standard -rectypes)))
diff --git a/ide/dune b/ide/dune
index 6931a747ac..037b0fcc9e 100644
--- a/ide/dune
+++ b/ide/dune
@@ -1,11 +1,34 @@
+; IDE Server
(ocamllex utf8_convert config_lexer coq_lex)
(library
(name core)
- (public_name coqide.core)
+ (public_name coqide-server.core)
(wrapped false)
- (modules (:standard \ idetop coqide_main))
- (libraries threads str lablgtk2.sourceview2 coq.lib coqide.protocol))
+ (modules document)
+ (libraries coq.lib))
+
+(executable
+ (name fake_ide)
+ (modules fake_ide)
+ (libraries coqide-server.protocol coqide-server.core))
+
+(executable
+ (name idetop)
+ (public_name coqidetop.opt)
+ (package coqide-server)
+ (modules idetop)
+ (libraries coq.toplevel coqide-server.protocol)
+ (link_flags -linkall))
+
+; IDE Client
+(library
+ (name gui)
+ (public_name coqide.gui)
+ (wrapped false)
+ (modules (:standard \ document fake_ide idetop coqide_main))
+ (optional)
+ (libraries coqide-server.protocol coqide-server.core lablgtk2.sourceview2))
(rule
(targets coqide_main.ml)
@@ -17,12 +40,4 @@
(public_name coqide)
(package coqide)
(modules coqide_main)
- (libraries coqide.core))
-
-(executable
- (name idetop)
- (public_name coqidetop.opt)
- (package coqide)
- (modules idetop)
- (libraries coq.toplevel coqide.protocol)
- (link_flags -linkall))
+ (libraries coqide.gui))
diff --git a/ide/dune-project b/ide/dune-project
deleted file mode 100644
index 948dc59000..0000000000
--- a/ide/dune-project
+++ /dev/null
@@ -1,3 +0,0 @@
-(lang dune 1.0)
-
-(name coqide-devel)
diff --git a/ide/dune-workspace b/ide/dune-workspace
deleted file mode 100644
index 38875eac2c..0000000000
--- a/ide/dune-workspace
+++ /dev/null
@@ -1,6 +0,0 @@
-(lang dune 1.2)
-
-; Add custom flags here. Default developer profile is `dev`
-(env
- (dev (flags :standard -rectypes -w -9-27-50+60))
- (release (flags :standard -rectypes)))
diff --git a/tools/fake_ide.ml b/ide/fake_ide.ml
index 0162011289..521aff6bf6 100644
--- a/tools/fake_ide.ml
+++ b/ide/fake_ide.ml
@@ -195,9 +195,9 @@ module GUILogic = struct
Document.unfocus doc;
ignore(Document.cut_at doc tip);
print_document ()
-
+
let at id id' _ = Stateid.equal id' id
-
+
let after_edit_at (id,need_unfocus) = function
| Interface.Fail (_,_,s) -> print_error s; exit 1
| Interface.Good (Util.Inl ()) ->
@@ -210,13 +210,13 @@ module GUILogic = struct
Document.focus doc ~cond_top:(at start_id) ~cond_bot:(at stop_id);
ignore(Document.cut_at doc id);
print_document ()
-
+
let get_id_pred pred =
try Document.find_id doc pred
with Not_found -> error "No state found"
let get_id id = get_id_pred (fun _ { name } -> name = id)
-
+
let after_fail coq = function
| Interface.Fail (safe_id,_,s) ->
prerr_endline "The command failed as expected";
diff --git a/ide/protocol/dune b/ide/protocol/dune
index 9ce4559940..801ceb20ec 100644
--- a/ide/protocol/dune
+++ b/ide/protocol/dune
@@ -1,6 +1,6 @@
(library
(name protocol)
- (public_name coqide.protocol)
+ (public_name coqide-server.protocol)
(wrapped false)
(libraries coq.lib))
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ff5e2bb5f3..ab57176643 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -153,11 +153,13 @@ let protect g e na =
if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
e',na
-let apply_cases_pattern ?loc ((ids,disjpat),id) c =
- let tm = DAst.make ?loc (GVar id) in
+let apply_cases_pattern_term ?loc (ids,disjpat) tm c =
let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in
DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
+let apply_cases_pattern ?loc (ids_disjpat,id) c =
+ apply_cases_pattern_term ?loc ids_disjpat (DAst.make ?loc (GVar id)) c
+
let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let lt x = DAst.make ?loc x in lt @@ match nc with
| NVar id -> GVar id
@@ -182,7 +184,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let e',disjpat,na = g e na in
(match disjpat with
| None -> GLetIn (na,f e b,Option.map (f e) t,f e' c)
- | Some disjpat -> DAst.get (apply_cases_pattern ?loc disjpat (f e' c)))
+ | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
| NCases (sty,rtntypopt,tml,eqnl) ->
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
let e',t' = match t with
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 003b49535f..819a66c190 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -359,7 +359,6 @@ type fconstr = {
and fterm =
| FRel of int
| FAtom of constr (* Metas and Sorts *)
- | FCast of fconstr * cast_kind * fconstr
| FFlex of table_key
| FInd of pinductive
| FConstruct of pconstructor
@@ -477,7 +476,7 @@ let rec lft_fconstr n ft =
| FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))}
| FLIFT(k,m) -> lft_fconstr (n+k) m
| FLOCKED -> assert false
- | FFlex _ | FAtom _ | FCast _ | FApp _ | FProj _ | FCaseT _ | FProd _
+ | FFlex _ | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _
| FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(n,ft)}
let lift_fconstr k f =
if Int.equal k 0 then f else lft_fconstr k f
@@ -558,8 +557,6 @@ let rec to_constr lfts v =
| FFlex (RelKey p) -> mkRel (reloc_rel p lfts)
| FFlex (VarKey x) -> mkVar x
| FAtom c -> exliftn lfts c
- | FCast (a,k,b) ->
- mkCast (to_constr lfts a, k, to_constr lfts b)
| FFlex (ConstKey op) -> mkConstU op
| FInd op -> mkIndU op
| FConstruct op -> mkConstructU op
@@ -866,7 +863,6 @@ let rec knh info m stk =
(match get_nth_arg m ri.(n) stk with
(Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
| (None, stk') -> (m,stk'))
- | FCast(t,_,_) -> knh info t stk
| FProj (p,c) ->
(match unfold_projection info p with
| None -> (m, stk)
@@ -951,7 +947,7 @@ let rec knr info tab m stk =
(match evar_value info.i_cache ev with
Some c -> knit info tab env c stk
| None -> (m,stk))
- | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _
+ | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FApp _ | FProj _
| FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _
| FCLOS _ -> (m, stk)
@@ -1031,7 +1027,7 @@ and norm_head info tab m =
mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
| FProj (p,c) ->
mkProj (p, kl info tab c)
- | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _
+ | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _
| FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m
(* Initialization and then normalization *)
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 6121b3a1ec..2a018d172a 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -131,7 +131,6 @@ type fconstr
type fterm =
| FRel of int
| FAtom of constr (** Metas and Sorts *)
- | FCast of fconstr * cast_kind * fconstr
| FFlex of table_key
| FInd of inductive Univ.puniverses
| FConstruct of constructor Univ.puniverses
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2abb4b485c..00576476ab 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -605,7 +605,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
| ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
| (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
- | (FLOCKED,_) | (_,FLOCKED) ) | (FCast _, _) | (_, FCast _) -> assert false
+ | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
| (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _
| FProd _ | FEvar _), _ -> raise NotConvertible
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index be79b8b07d..a56a8314e6 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -137,7 +137,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
infer_stack infos variances stk
(* Removed by whnf *)
- | FLOCKED | FCaseT _ | FCast _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false
+ | FLOCKED | FCaseT _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false
and infer_stack infos variances (stk:CClosure.stack) =
match stk with
diff --git a/test-suite/bugs/closed/8672.v b/test-suite/bugs/closed/8672.v
new file mode 100644
index 0000000000..66cd6dfa8c
--- /dev/null
+++ b/test-suite/bugs/closed/8672.v
@@ -0,0 +1,5 @@
+(* Was generating a dangling "pat" variable at some time *)
+
+Notation "'plet' x := e 'in' t" :=
+ ((fun H => let x := id H in t) e) (at level 0, x pattern).
+Definition bla := plet (pair x y) := pair 1 2 in x.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 04:31:38 +0000