aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml9
-rw-r--r--README.md3
-rwxr-xr-xdev/ci/ci-basic-overlay.sh7
-rwxr-xr-xdev/ci/ci-fiat-crypto-legacy.sh4
-rw-r--r--doc/tools/coqrst/coqdomain.py1
-rw-r--r--lib/system.ml6
-rw-r--r--lib/system.mli2
-rw-r--r--stm/stm.ml11
-rw-r--r--test-suite/Makefile5
-rw-r--r--test-suite/bugs/opened/bug_3166.v1
-rw-r--r--test-suite/bugs/opened/bug_3754.v1
-rw-r--r--test-suite/bugs/opened/bug_3890.v2
-rw-r--r--test-suite/bugs/opened/bug_3938.v1
-rw-r--r--test-suite/output-modulo-time/ltacprof_cutoff.v2
-rw-r--r--toplevel/vernac.ml29
-rw-r--r--vernac/topfmt.ml21
-rw-r--r--vernac/topfmt.mli1
-rw-r--r--vernac/vernacentries.ml5
18 files changed, 66 insertions, 45 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index f54f64bf28..c11ba11fc5 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -151,7 +151,7 @@ after_script:
- BIN=$(readlink -f ../_install_ci/bin)/
- LIB=$(readlink -f ../_install_ci/lib/coq)/
- export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH"
- - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all
+ - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" COQFLAGS="${COQFLAGS}" all
artifacts:
name: "$CI_JOB_NAME.logs"
when: on_failure
@@ -427,6 +427,13 @@ test-suite:edge+trunk+dune:
expire_in: 1 week
allow_failure: true
+test-suite:base+async:
+ <<: *test-suite-template
+ dependencies:
+ - build:base
+ variables:
+ COQFLAGS: "-async-proofs on"
+
validate:base:
<<: *validate-template
dependencies:
diff --git a/README.md b/README.md
index e6a52e95e3..9ee8e9cb47 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,7 @@
# Coq
-[![pipeline status](https://gitlab.com/coq/coq/badges/master/pipeline.svg)](https://gitlab.com/coq/coq/commits/master)
+[![GitLab](https://gitlab.com/coq/coq/badges/master/pipeline.svg)](https://gitlab.com/coq/coq/commits/master)
+[![Azure Pipelines](https://dev.azure.com/coq/coq/_apis/build/status/coq.coq?branchName=master)](https://dev.azure.com/coq/coq/_build/latest?definitionId=1?branchName=master)
[![Travis](https://travis-ci.org/coq/coq.svg?branch=master)](https://travis-ci.org/coq/coq/builds)
[![Appveyor](https://ci.appveyor.com/api/projects/status/eln43k05pa2vm908/branch/master?svg=true)](https://ci.appveyor.com/project/coq/coq/branch/master)
[![Gitter](https://badges.gitter.im/coq/coq.svg)](https://gitter.im/coq/coq)
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index e74a7853b9..6944324729 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -150,6 +150,13 @@
: "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}"
########################################################################
+# fiat_crypto_legacy
+########################################################################
+: "${fiat_crypto_legacy_CI_REF:=sp2019latest}"
+: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}"
+: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}"
+
+########################################################################
# coq_dpdgraph
########################################################################
: "${coq_dpdgraph_CI_REF:=coq-master}"
diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh
index 6bf3138346..2af4b58201 100755
--- a/dev/ci/ci-fiat-crypto-legacy.sh
+++ b/dev/ci/ci-fiat-crypto-legacy.sh
@@ -4,11 +4,11 @@ ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
FORCE_GIT=1
-git_download fiat_crypto
+git_download fiat_crypto_legacy
fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display"
fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display"
-( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
+( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \
./etc/ci/remove_autogenerated.sh && \
make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} )
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 827b7c13c1..067af954ad 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -1189,7 +1189,6 @@ def setup(app):
app.connect('doctree-resolved', CoqtopBlocksTransform.merge_consecutive_coqtop_blocks)
# Add extra styles
- app.add_stylesheet("fonts.css")
app.add_stylesheet("ansi.css")
app.add_stylesheet("coqdoc.css")
app.add_javascript("notations.js")
diff --git a/lib/system.ml b/lib/system.ml
index a9db95318f..fd6579dd69 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -287,20 +287,20 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) =
real (round (sstop -. sstart)) ++ str "s" ++
str ")"
-let with_time ~batch f x =
+let with_time ~batch ~header f x =
let tstart = get_time() in
let msg = if batch then "" else "Finished transaction in " in
try
let y = f x in
let tend = get_time() in
let msg2 = if batch then "" else " (successful)" in
- Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+ Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
y
with e ->
let tend = get_time() in
let msg = if batch then "" else "Finished failing transaction in " in
let msg2 = if batch then "" else " (failure)" in
- Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+ Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
raise e
(* We use argv.[0] as we don't want to resolve symlinks *)
diff --git a/lib/system.mli b/lib/system.mli
index a3b79ee528..6dd1eb5a84 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -105,7 +105,7 @@ val time_difference : time -> time -> float (** in seconds *)
val fmt_time_difference : time -> time -> Pp.t
-val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b
+val with_time : batch:bool -> header:Pp.t -> ('a -> 'b) -> 'a -> 'b
(** [get_toplevel_path program] builds a complete path to the
executable denoted by [program]. This involves:
diff --git a/stm/stm.ml b/stm/stm.ml
index 7e4ee38547..036b8d7969 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2016,7 +2016,7 @@ end = struct (* {{{ *)
find ~time:false ~batch:false ~fail:false e in
let st = Vernacstate.freeze_interp_state ~marshallable:false in
Vernacentries.with_fail st fail (fun () ->
- (if time then System.with_time ~batch else (fun x -> x)) (fun () ->
+ (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
ignore(TaskQueue.with_n_workers nworkers (fun queue ->
Proof_global.with_current_proof (fun _ p ->
let Proof.{goals} = Proof.data p in
@@ -2992,7 +2992,14 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
(* Unknown: we execute it, check for open goals and propagate sideeff *)
| VtUnknown, VtNow ->
let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
- let id = VCS.new_node ~id:newtip () in
+ if not (get_allow_nested_proofs ()) && in_proof then
+ "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on."
+ |> Pp.str
+ |> (fun s -> (UserError (None, s), Exninfo.null))
+ |> State.exn_on ~valid:Stateid.dummy Stateid.dummy
+ |> Exninfo.iraise
+ else
+ let id = VCS.new_node ~id:newtip () in
let head_id = VCS.get_branch_pos head in
let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *)
let step () =
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 34a1900bbc..37091a49e5 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -36,9 +36,10 @@ include ../Makefile.common
# easily overridden
LIB := ..
BIN := $(shell cd ..; pwd)/bin/
+COQFLAGS?=
-coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite
-coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
+coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite $(COQFLAGS)
+coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS)
coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
coqdoc := $(BIN)coqdoc
coqtopbyte := $(BIN)coqtop.byte
diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v
index e1c29a954c..baf87631f0 100644
--- a/test-suite/bugs/opened/bug_3166.v
+++ b/test-suite/bugs/opened/bug_3166.v
@@ -81,3 +81,4 @@ Goal forall T (x y : T) (p : x = y), True.
compute in H0.
change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0.
Fail pose proof (fun k => @eq_trans _ _ _ k H0).
+Abort.
diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v
index a717bbe735..18820b1a4c 100644
--- a/test-suite/bugs/opened/bug_3754.v
+++ b/test-suite/bugs/opened/bug_3754.v
@@ -282,3 +282,4 @@ Defined.
rewrite <- ap_p_pp; rewrite_moveL_Mp_p.
Set Debug Tactic Unification.
Fail rewrite (concat_Ap ff2).
+ Abort.
diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v
index 5c74addb62..78b2aa69b9 100644
--- a/test-suite/bugs/opened/bug_3890.v
+++ b/test-suite/bugs/opened/bug_3890.v
@@ -1,3 +1,5 @@
+Set Nested Proofs Allowed.
+
Class Foo.
Class Bar := b : Type.
diff --git a/test-suite/bugs/opened/bug_3938.v b/test-suite/bugs/opened/bug_3938.v
index 2d0d1930f1..3c7c945ed8 100644
--- a/test-suite/bugs/opened/bug_3938.v
+++ b/test-suite/bugs/opened/bug_3938.v
@@ -4,3 +4,4 @@ Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b.
intros a b f H.
rewrite H. (* Toplevel input, characters 15-25:
Anomaly: Evar ?X11 was not declared. Please report. *)
+Abort.
diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v
index ae5d51bae8..b7c98aa134 100644
--- a/test-suite/output-modulo-time/ltacprof_cutoff.v
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-profile-ltac") -*- *)
+(* -*- coq-prog-args: ("-async-proofs" "off" "-profile-ltac") -*- *)
Require Coq.ZArith.BinInt.
Module WithIdTac.
Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac).
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c914bbecff..d8465aac27 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -37,34 +37,6 @@ let vernac_echo ?loc in_chan = let open Loc in
Feedback.msg_notice @@ str @@ really_input_string in_chan len
) loc
-(* For coqtop -time, we display the position in the file,
- and a glimpse of the executed command *)
-
-let pp_cmd_header {CAst.loc;v=com} =
- let shorten s =
- if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
- in
- let noblank s = String.map (fun c ->
- match c with
- | ' ' | '\n' | '\t' | '\r' -> '~'
- | x -> x
- ) s
- in
- let (start,stop) = Option.cata Loc.unloc (0,0) loc in
- let safe_pr_vernac x =
- try Ppvernac.pr_vernac x
- with e -> str (Printexc.to_string e) in
- let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
- in str "Chars " ++ int start ++ str " - " ++ int stop ++
- str " [" ++ str cmd ++ str "] "
-
-(* This is a special case where we assume we are in console batch mode
- and take control of the console.
- *)
-let print_cmd_header com =
- Pp.pp_with !Topfmt.std_ft (pp_cmd_header com);
- Format.pp_print_flush !Topfmt.std_ft ()
-
(* Reenable when we get back to feedback printing *)
(* let is_end_of_input any = match any with *)
(* Stm.End_of_input -> true *)
@@ -88,7 +60,6 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
due to the way it prints. *)
let com = if state.time
then begin
- print_cmd_header com;
CAst.make ?loc @@ VernacTime(state.time,com)
end else com in
let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 4065bb9c1f..b4b893a3fd 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -406,3 +406,24 @@ let with_output_to_file fname func input =
deep_ft := Util.pi3 old_fmt;
close_out channel;
Exninfo.iraise reraise
+
+(* For coqtop -time, we display the position in the file,
+ and a glimpse of the executed command *)
+
+let pr_cmd_header {CAst.loc;v=com} =
+ let shorten s =
+ if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
+ in
+ let noblank s = String.map (fun c ->
+ match c with
+ | ' ' | '\n' | '\t' | '\r' -> '~'
+ | x -> x
+ ) s
+ in
+ let (start,stop) = Option.cata Loc.unloc (0,0) loc in
+ let safe_pr_vernac x =
+ try Ppvernac.pr_vernac x
+ with e -> str (Printexc.to_string e) in
+ let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
+ in str "Chars " ++ int start ++ str " - " ++ int stop ++
+ str " [" ++ str cmd ++ str "] "
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 0ddf474970..5f84c5edee 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -71,3 +71,4 @@ val print_err_exn : exn -> unit
redirected to a file [file] *)
val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+val pr_cmd_header : Vernacexpr.vernac_control CAst.t -> Pp.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e6e3db4beb..dbccea1117 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2388,8 +2388,9 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
control v
| VernacRedirect (s, {v}) ->
Topfmt.with_output_to_file s control v
- | VernacTime (batch, {v}) ->
- System.with_time ~batch control v;
+ | VernacTime (batch, com) ->
+ let header = if batch then Topfmt.pr_cmd_header com else Pp.mt () in
+ System.with_time ~batch ~header control com.CAst.v;
and aux ~atts : _ -> unit =
function
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 16:32:22 +0000