diff options
82 files changed, 447 insertions, 519 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1c5c8efc19..7dda19192d 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -362,7 +362,7 @@ validate:edge+flambda: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" -ci-aac-tactics: +ci-aac_tactics: <<: *ci-template ci-bedrock2: @@ -378,7 +378,7 @@ ci-color: ci-compcert: <<: *ci-template-flambda -ci-coq-dpdgraph: +ci-coq_dpdgraph: <<: *ci-template ci-coquelicot: @@ -438,7 +438,7 @@ ci-paramcoq: ci-pidetop: <<: *ci-template -ci-plugin-tutorial: +ci-plugin_tutorial: <<: *ci-template ci-quickchick: diff --git a/CHANGES.md b/CHANGES.md index d7f2107d1f..6438cf2571 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -67,6 +67,8 @@ Vernacular commands - Binders for an `Instance` now act more like binders for a `Theorem`. Names may not be repeated, and may not overlap with section variable names. +- Removed the deprecated `Implicit Tactic` family of commands. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: @@ -97,6 +99,11 @@ Standard Library Imported. This should be relevant only when importing files which don't use -noinit into files which do. +Universes + +- Added `Print Universes Subgraph` variant of `Print Universes`. + Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).` + Changes from 8.8.2 to 8.9+beta1 =============================== diff --git a/Makefile.ci b/Makefile.ci index e8fea11bdb..88ea64974a 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -9,12 +9,12 @@ ########################################################################## CI_TARGETS= \ - ci-aac-tactics \ + ci-aac_tactics \ ci-bedrock2 \ ci-bignums \ ci-color \ ci-compcert \ - ci-coq-dpdgraph \ + ci-coq_dpdgraph \ ci-coquelicot \ ci-corn \ ci-cpdt \ @@ -38,7 +38,7 @@ CI_TARGETS= \ ci-mtac2 \ ci-paramcoq \ ci-pidetop \ - ci-plugin-tutorial \ + ci-plugin_tutorial \ ci-quickchick \ ci-sf \ ci-simple-io \ diff --git a/clib/dyn.ml b/clib/dyn.ml index 6c45767246..22c49706be 100644 --- a/clib/dyn.ml +++ b/clib/dyn.ml @@ -38,6 +38,7 @@ sig type t = Dyn : 'a tag * 'a -> t val create : string -> 'a tag + val anonymous : int -> 'a tag val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option val repr : 'a tag -> string @@ -81,15 +82,22 @@ module Self : PreS = struct let create (s : string) = let hash = Hashtbl.hash s in - let () = - if Int.Map.mem hash !dyntab then - let old = Int.Map.find hash !dyntab in - let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in - assert false - in - let () = dyntab := Int.Map.add hash s !dyntab in + if Int.Map.mem hash !dyntab then begin + let old = Int.Map.find hash !dyntab in + Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old; + assert false + end; + dyntab := Int.Map.add hash s !dyntab; hash + let anonymous n = + if Int.Map.mem n !dyntab then begin + Printf.eprintf "Dynamic tag collision: %d\n%!" n; + assert false + end; + dyntab := Int.Map.add n "<anonymous>" !dyntab; + n + let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option = fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None diff --git a/clib/dyn.mli b/clib/dyn.mli index ff9762bd6b..1bd78b2db8 100644 --- a/clib/dyn.mli +++ b/clib/dyn.mli @@ -48,6 +48,12 @@ sig Type names are hashed, so [create] may raise even if no type with the exact same name was registered due to a collision. *) + val anonymous : int -> 'a tag + (** [anonymous i] returns a tag describing an [i]-th anonymous type. + If [anonymous] is not used together with [create], [max_int] anonymous types + are available. + [anonymous] raises an exception if [i] is already registered. *) + val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option (** [eq t1 t2] returns [Some witness] if [t1] is the same as [t2], [None] otherwise. *) diff --git a/clib/store.ml b/clib/store.ml index 1469358c9d..79e26908d7 100644 --- a/clib/store.ml +++ b/clib/store.ml @@ -20,70 +20,37 @@ module type S = sig type t type 'a field + val field : unit -> 'a field val empty : t val set : t -> 'a field -> 'a -> t val get : t -> 'a field -> 'a option val remove : t -> 'a field -> t val merge : t -> t -> t - val field : unit -> 'a field end -module Make () : S = +module Make() : S = struct - - let next = - let count = ref 0 in fun () -> - let n = !count in - incr count; - n - - type t = Obj.t option array - (** Store are represented as arrays. For small values, which is typicial, - is slightly quicker than other implementations. *) - -type 'a field = int - -let allocate len : t = Array.make len None - -let empty : t = [||] - -let set (s : t) (i : 'a field) (v : 'a) : t = - let len = Array.length s in - let nlen = if i < len then len else succ i in - let () = assert (0 <= i) in - let ans = allocate nlen in - Array.blit s 0 ans 0 len; - Array.unsafe_set ans i (Some (Obj.repr v)); - ans - -let get (s : t) (i : 'a field) : 'a option = - let len = Array.length s in - if len <= i then None - else Obj.magic (Array.unsafe_get s i) - -let remove (s : t) (i : 'a field) = - let len = Array.length s in - let () = assert (0 <= i) in - let ans = allocate len in - Array.blit s 0 ans 0 len; - if i < len then Array.unsafe_set ans i None; - ans - -let merge (s1 : t) (s2 : t) : t = - let len1 = Array.length s1 in - let len2 = Array.length s2 in - let nlen = if len1 < len2 then len2 else len1 in - let ans = allocate nlen in - (** Important: No more allocation from here. *) - Array.blit s2 0 ans 0 len2; - for i = 0 to pred len1 do - let v = Array.unsafe_get s1 i in - match v with - | None -> () - | Some _ -> Array.unsafe_set ans i v - done; - ans - -let field () = next () - + module Dyn = Dyn.Make() + module Map = Dyn.Map(struct type 'a t = 'a end) + + type t = Map.t + type 'a field = 'a Dyn.tag + + let next = ref 0 + let field () = + let f = Dyn.anonymous !next in + incr next; + f + + let empty = + Map.empty + let set s f v = + Map.add f v s + let get s f = + try Some (Map.find f s) + with Not_found -> None + let remove s f = + Map.remove f s + let merge s1 s2 = + Map.fold (fun (Map.Any (f, v)) s -> Map.add f v s) s1 s2 end diff --git a/clib/store.mli b/clib/store.mli index 0c2b2e0856..7cdd1d3bed 100644 --- a/clib/store.mli +++ b/clib/store.mli @@ -19,6 +19,9 @@ sig type 'a field (** Type of field of such stores *) + val field : unit -> 'a field + (** Create a new field *) + val empty : t (** Empty store *) @@ -33,11 +36,7 @@ sig val merge : t -> t -> t (** [merge s1 s2] adds all the fields of [s1] into [s2]. *) - - val field : unit -> 'a field - (** Create a new field *) - end -module Make () : S +module Make() : S (** Create a new store type. *) diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 71207bb040..0dcabc0b97 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1645,7 +1645,7 @@ function make_addon_bignums { function make_addon_equations { installer_addon_dependency equations - if build_prep_overlay Equations; then + if build_prep_overlay equations; then installer_addon_section equations "Equations" "Coq plugin for defining functions by equations" "" # Note: PATH is automatically saved/restored by build_prep / build_post PATH=$COQBIN:$PATH diff --git a/dev/ci/ci-aac-tactics.sh b/dev/ci/ci-aac-tactics.sh deleted file mode 100755 index 896a0ddf66..0000000000 --- a/dev/ci/ci-aac-tactics.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/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-aac_tactics.sh b/dev/ci/ci-aac_tactics.sh new file mode 100755 index 0000000000..19f1f43746 --- /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 aac_tactics + +( cd "${CI_BUILD_DIR}/aac_tactics" && make && make install ) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 3137576207..4d5834eeb6 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -113,16 +113,16 @@ ######################################################################## # CompCert ######################################################################## -: "${CompCert_CI_REF:=master}" -: "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert}" -: "${CompCert_CI_ARCHIVEURL:=${CompCert_CI_GITURL}/archive}" +: "${compcert_CI_REF:=master}" +: "${compcert_CI_GITURL:=https://github.com/AbsInt/CompCert}" +: "${compcert_CI_ARCHIVEURL:=${compcert_CI_GITURL}/archive}" ######################################################################## # VST ######################################################################## -: "${VST_CI_REF:=master}" -: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" -: "${VST_CI_ARCHIVEURL:=${VST_CI_GITURL}/archive}" +: "${vst_CI_REF:=master}" +: "${vst_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" +: "${vst_CI_ARCHIVEURL:=${vst_CI_GITURL}/archive}" ######################################################################## # cross-crypto @@ -153,7 +153,7 @@ : "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" ######################################################################## -# coq-dpdgraph +# coq_dpdgraph ######################################################################## : "${coq_dpdgraph_CI_REF:=coq-master}" : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}" @@ -162,9 +162,9 @@ ######################################################################## # CoLoR ######################################################################## -: "${CoLoR_CI_REF:=master}" -: "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color}" -: "${CoLoR_CI_ARCHIVEURL:=${CoLoR_CI_GITURL}/archive}" +: "${color_CI_REF:=master}" +: "${color_CI_GITURL:=https://github.com/fblanqui/color}" +: "${color_CI_ARCHIVEURL:=${color_CI_GITURL}/archive}" ######################################################################## # SF @@ -196,16 +196,16 @@ ######################################################################## # Equations ######################################################################## -: "${Equations_CI_REF:=master}" -: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" -: "${Equations_CI_ARCHIVEURL:=${Equations_CI_GITURL}/archive}" +: "${equations_CI_REF:=master}" +: "${equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" +: "${equations_CI_ARCHIVEURL:=${equations_CI_GITURL}/archive}" ######################################################################## # Elpi ######################################################################## -: "${Elpi_CI_REF:=coq-master}" -: "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" -: "${Elpi_CI_ARCHIVEURL:=${Elpi_CI_GITURL}/archive}" +: "${elpi_CI_REF:=coq-master}" +: "${elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" +: "${elpi_CI_ARCHIVEURL:=${elpi_CI_GITURL}/archive}" ######################################################################## # fcsl-pcm @@ -257,11 +257,11 @@ : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" ######################################################################## -# aac-tactics +# aac_tactics ######################################################################## -: "${aactactics_CI_REF:=master}" -: "${aactactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}" -: "${aactactics_CI_ARCHIVEURL:=${aactactics_CI_GITURL}/archive}" +: "${aac_tactics_CI_REF:=master}" +: "${aac_tactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}" +: "${aac_tactics_CI_ARCHIVEURL:=${aac_tactics_CI_GITURL}/archive}" ######################################################################## # paramcoq diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index dc696f69d9..a0094b1006 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download CoLoR +git_download color -( cd "${CI_BUILD_DIR}/CoLoR" && make ) +( cd "${CI_BUILD_DIR}/color" && make ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 7a450d0d48..a5aa54144c 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -46,8 +46,11 @@ for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null . "${overlay}" done + +set +x # shellcheck source=ci-basic-overlay.sh . "${ci_dir}/ci-basic-overlay.sh" +set -x # [git_download project] will download [project] and unpack it # in [$CI_BUILD_DIR/project] if the folder does not exist already; diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 01c35ceb4a..59a85e4726 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -3,7 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download CompCert +git_download compcert -( cd "${CI_BUILD_DIR}/CompCert" && \ +( cd "${CI_BUILD_DIR}/compcert" && \ ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq_dpdgraph.sh index 2373ea6c62..2373ea6c62 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq_dpdgraph.sh diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh index 9b4a06fd5b..d60bf34ba2 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download Elpi +git_download elpi -( cd "${CI_BUILD_DIR}/Elpi" && make && make install ) +( cd "${CI_BUILD_DIR}/elpi" && make && make install ) diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 998d50faa7..b58a794da2 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -3,7 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download Equations +git_download equations -( cd "${CI_BUILD_DIR}/Equations" && coq_makefile -f _CoqProject -o Makefile && \ +( cd "${CI_BUILD_DIR}/equations" && coq_makefile -f _CoqProject -o Makefile && \ make && make test-suite && make examples && make install) diff --git a/dev/ci/ci-plugin-tutorial.sh b/dev/ci/ci-plugin_tutorial.sh index 6c26a71a21..6c26a71a21 100755 --- a/dev/ci/ci-plugin-tutorial.sh +++ b/dev/ci/ci-plugin_tutorial.sh diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 0fec19205a..169d1a41db 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download VST +git_download vst -( cd "${CI_BUILD_DIR}/VST" && make IGNORECOQVERSION=true ) +( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true ) diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh deleted file mode 100644 index d812df3ec0..0000000000 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_REF=ssr-merge - mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp -fi diff --git a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh deleted file mode 100644 index 575df07425..0000000000 --- a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh +++ /dev/null @@ -1,8 +0,0 @@ -_OVERLAY_BRANCH=pure-sharing-flag - -if [ "$CI_PULL_REQUEST" = "7085" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - mtac2_CI_BRANCH="$_OVERLAY_BRANCH" - mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 - -fi diff --git a/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh b/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh deleted file mode 100644 index 019cb8054d..0000000000 --- a/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "7257" ] || [ "$CI_BRANCH" = "master+fix-yet-another-unif-dep-in-alphabet" ]; then - cross_crypto_CI_REF=master+fix-coq7257-ascii-sensitive-unification - cross_crypto_CI_GITURL=https://github.com/herbelin/cross-crypto -fi diff --git a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh b/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh deleted file mode 100644 index 3a6480a5a1..0000000000 --- a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "7288" ] || [ "$CI_BRANCH" = "master+new-module-pretyping-id-management" ]; then - - ltac2_CI_BRANCH=master+globenv-coq-pr7288 - ltac2_CI_GITURL=https://github.com/herbelin/ltac2 - -fi diff --git a/dev/ci/user-overlays/08456-fix-6764.sh b/dev/ci/user-overlays/08456-fix-6764.sh deleted file mode 100644 index 3b951d9c07..0000000000 --- a/dev/ci/user-overlays/08456-fix-6764.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8456" ] || [ "$CI_BRANCH" = "fix-6764" ]; then - Elpi_CI_REF=overlay/8456 -fi diff --git a/dev/ci/user-overlays/08515-command-atts.sh b/dev/ci/user-overlays/08515-command-atts.sh deleted file mode 100755 index 4605255d5e..0000000000 --- a/dev/ci/user-overlays/08515-command-atts.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8515" ] || [ "$CI_BRANCH" = "command-atts" ]; then - ltac2_CI_REF=command-atts - ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 - - Equations_CI_REF=command-atts - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - plugin_tutorial_CI_REF=command-atts - plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials -fi diff --git a/dev/ci/user-overlays/08552-gares-elpi-11.sh b/dev/ci/user-overlays/08552-gares-elpi-11.sh deleted file mode 100644 index c08f44fc50..0000000000 --- a/dev/ci/user-overlays/08552-gares-elpi-11.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8552" ] || [ "$CI_BRANCH" = "elpi-1.1" ]; then - Elpi_CI_REF=coq-master-elpi-1.1 -fi diff --git a/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh b/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh deleted file mode 100644 index 484ad8f9e6..0000000000 --- a/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh +++ /dev/null @@ -1,11 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8554" ] || [ "$CI_BRANCH" = "master+fix8553-change-under-binders" ]; then - - ltac2_CI_BRANCH=master+fix-pr8554-change-takes-env - ltac2_CI_REF=master+fix-pr8554-change-takes-env - ltac2_CI_GITURL=https://github.com/herbelin/ltac2 - - Equations_CI_BRANCH=master+fix-pr8554-change-takes-env - Equations_CI_REF=master+fix-pr8554-change-takes-env - Equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh deleted file mode 100644 index 41c2ad6fef..0000000000 --- a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8555" ] || [ "$CI_BRANCH" = "rm-section-path" ]; then - - ltac2_CI_REF=rm-section-path - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - Equations_CI_REF=rm-section-path - Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08601-name-abstract-univ-context.sh b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh deleted file mode 100644 index 9d723dc7f2..0000000000 --- a/dev/ci/user-overlays/08601-name-abstract-univ-context.sh +++ /dev/null @@ -1,11 +0,0 @@ -_OVERLAY_BRANCH=name-abstract-univ-context - -if [ "$CI_PULL_REQUEST" = "8601" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - Elpi_CI_REF="$_OVERLAY_BRANCH" - Elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - Equations_CI_REF="$_OVERLAY_BRANCH" - Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh deleted file mode 100644 index bd3e1bf7ff..0000000000 --- a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8741" ] || [ "$CI_BRANCH" = "typeclasses-functional-evar_map" ]; then - plugin_tutorial_CI_REF=pr8671-fix - plugin_tutorial_CI_GITURL=https://github.com/mattam82/plugin_tutorials - -fi diff --git a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh deleted file mode 100644 index 98530c825a..0000000000 --- a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8684" ] || [ "$CI_BRANCH" = "kernel-entries-cleanup" ]; then - - Elpi_CI_REF=kernel-entries-cleanup - Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi - - Equations_CI_REF=kernel-entries-cleanup - Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh deleted file mode 100644 index 81ed91f52b..0000000000 --- a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8688" ] || [ "$CI_BRANCH" = "master+generalizing-evar-map-printer-over-env" ]; then - - Elpi_CI_REF=master+generalized-evar-printers-pr8688 - Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - -fi diff --git a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh deleted file mode 100644 index b3a9f67e00..0000000000 --- a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8704" ] || [ "$CI_BRANCH" = "vernac+monify_hook" ]; then - - # ltac2_CI_REF=rm-section-path - # ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - plugin_tutorial_CI_REF=vernac+monify_hook - plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials - - Elpi_CI_REF=vernac+monify_hook - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - Equations_CI_REF=vernac+monify_hook - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08844-split-tactics.sh b/dev/ci/user-overlays/08844-split-tactics.sh deleted file mode 100644 index 8ad8cba243..0000000000 --- a/dev/ci/user-overlays/08844-split-tactics.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8844" ] || [ "$CI_BRANCH" = "split-tactics" ]; then - Equations_CI_REF=split-tactics - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - ltac2_CI_REF=split-tactics - ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 - - fiat_parsers_CI_REF=split-tactics - fiat_parsers_CI_GITURL=https://github.com/SkySkimmer/fiat -fi diff --git a/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh new file mode 100644 index 0000000000..1c5157ba12 --- /dev/null +++ b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8914" ] || [ "$CI_BRANCH" = "lib+better_boot_coqproject" ]; then + + quickchick_CI_REF=lib+better_boot_coqproject + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh deleted file mode 100644 index 76aa37d380..0000000000 --- a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh +++ /dev/null @@ -1,5 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then - HoTT_CI_REF=fix-for-numeral-notations - HoTT_CI_GITURL=https://github.com/JasonGross/HoTT - HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive -fi diff --git a/dev/tools/create_overlays.sh b/dev/tools/create_overlays.sh new file mode 100755 index 0000000000..314ac07e68 --- /dev/null +++ b/dev/tools/create_overlays.sh @@ -0,0 +1,78 @@ +#!/usr/bin/env bash + +# TODO: +# +# - Check if the branch already exists in the remote => checkout +# - Better error handling +# - Just checkout, don't build +# - Rebase functionality +# + +set -x +set -e +set -o pipefail + +# setup_contrib_git("_build_ci/fiat", "https://github.com/ejgallego/fiat-core.git") +setup_contrib_git() { + + local _DIR=$1 + local _GITURL=$2 + + ( cd $_DIR + git checkout -b $OVERLAY_BRANCH || true # allow the branch to exist already + git remote add $DEVELOPER_NAME $_GITURL || true # allow the remote to exist already + ) + +} + +if [ $# -lt 3 ]; then + echo "usage: $0 github_username pr_number contrib1 ... contribN" + exit 1 +fi + +set +x +. dev/ci/ci-basic-overlay.sh +set -x + +DEVELOPER_NAME=$1 +shift +PR_NUMBER=$1 +shift +OVERLAY_BRANCH=$(git rev-parse --abbrev-ref HEAD) +OVERLAY_FILE=$(mktemp overlay-XXXX) + +# Create the overlay file +printf 'if [ "$CI_PULL_REQUEST" = "%s" ] || [ "$CI_BRANCH" = "%s" ]; then \n\n' "$PR_NUMBER" "$OVERLAY_BRANCH" > "$OVERLAY_FILE" + +# We first try to build the contribs +while test $# -gt 0 +do + _CONTRIB_NAME=$1 + _CONTRIB_GITURL=${_CONTRIB_NAME}_CI_GITURL + _CONTRIB_GITURL=${!_CONTRIB_GITURL} + echo "Processing Contrib $_CONTRIB_NAME" + + # check _CONTRIB_GIT exists and it is of the from github... + + _CONTRIB_DIR=_build_ci/$_CONTRIB_NAME + + # extract the relevant part of the repository + _CONTRIB_GITSUFFIX=${_CONTRIB_GITURL#https://github.com/*/} + _CONTRIB_GITURL="https://github.com/$DEVELOPER_NAME/$_CONTRIB_GITSUFFIX" + _CONTRIB_GITPUSHURL="git@github.com:$DEVELOPER_NAME/${_CONTRIB_GITSUFFIX}.git" + + # This should work better: for example we should be able not to + # build but just to checkout. + make ci-$_CONTRIB_NAME || true + setup_contrib_git $_CONTRIB_DIR $_CONTRIB_GITPUSHURL + + echo " ${_CONTRIB_NAME}_CI_REF=$OVERLAY_BRANCH" >> $OVERLAY_FILE + echo " ${_CONTRIB_NAME}_CI_GITURL=$_CONTRIB_GITURL" >> $OVERLAY_FILE + echo "" >> $OVERLAY_FILE + shift +done + +# End the file; copy to overlays folder. +echo "fi" >> $OVERLAY_FILE +PR_NUMBER=$(printf '%05d' "$PR_NUMBER") +mv $OVERLAY_FILE dev/ci/user-overlays/$PR_NUMBER-$DEVELOPER_NAME-$OVERLAY_BRANCH.sh diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 9dae7fd102..391afcb1f7 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2155,6 +2155,12 @@ If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT language, and can be processed by Graphviz tools. The format is unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. +.. cmdv:: Print Universes Subgraph(@names) + +Prints the graph restricted to the requested names (adjusting +constraints to preserve the implied transitive constraints between +kept universes). + .. _existential-variables: Existential variables @@ -2247,7 +2253,3 @@ expression as described in :ref:`ltac`. This construction is useful when one wants to define complicated terms using highly automated tactics without resorting to writing the proof-term by means of the interactive proof engine. - -This mechanism is comparable to the ``Declare Implicit Tactic`` command -defined at :ref:`tactics-implicit-automation`, except that the used -tactic is local to each hole instead of being declared globally. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 457f9b2efa..041f1bc966 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3745,32 +3745,6 @@ Setting implicit automation tactics Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` - .. cmd:: Declare Implicit Tactic @tactic - - This command declares a tactic to be used to solve implicit arguments - that Coq does not know how to solve by unification. It is used every - time the term argument of a tactic has one of its holes not fully - resolved. - - .. deprecated:: 8.9 - - This command is deprecated. Use :ref:`typeclasses <typeclasses>` or - :ref:`tactics-in-terms <tactics-in-terms>` instead. - - .. example:: - - .. coqtop:: all - - Parameter quo : nat -> forall n:nat, n<>0 -> nat. - Notation "x // y" := (quo x y _) (at level 40). - Declare Implicit Tactic assumption. - Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. - intros. - exists (n // m). - - The tactic ``exists (n // m)`` did not fail. The hole was solved - by ``assumption`` so that it behaved as ``exists (quo n m H)``. - .. _decisionprocedures: Decision procedures diff --git a/ide/.merlin.in b/ide/.merlin.in index 953b5dce4c..4dc6f45550 100644 --- a/ide/.merlin.in +++ b/ide/.merlin.in @@ -2,5 +2,7 @@ PKG unix laglgtk2 lablgtk2.sourceview2 S utils B utils +S protocol +B protocol REC diff --git a/ide/configwin.ml b/ide/configwin.ml index 69e8b647ae..24be721631 100644 --- a/ide/configwin.ml +++ b/ide/configwin.ml @@ -46,6 +46,6 @@ let modifiers = Configwin_ihm.modifiers let edit ?(apply=(fun () -> ())) - title ?width ?height + title ?parent ?width ?height conf_struct_list = - Configwin_ihm.edit ~with_apply: true ~apply title ?width ?height conf_struct_list + Configwin_ihm.edit ~with_apply: true ~apply title ?parent ?width ?height conf_struct_list diff --git a/ide/configwin.mli b/ide/configwin.mli index 7616e471db..0ee77d69b5 100644 --- a/ide/configwin.mli +++ b/ide/configwin.mli @@ -158,6 +158,7 @@ val custom : ?label: string -> GPack.box -> (unit -> unit) -> bool -> parameter_ val edit : ?apply: (unit -> unit) -> string -> + ?parent:GWindow.window -> ?width:int -> ?height:int -> configuration_structure list -> diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml index d16efa603d..91695e944e 100644 --- a/ide/configwin_ihm.ml +++ b/ide/configwin_ihm.ml @@ -662,12 +662,13 @@ class configuration_box (tt : GData.tooltips) conf_struct = to configure the various parameters. *) let edit ?(with_apply=true) ?(apply=(fun () -> ())) - title ?width ?height + title ?parent ?width ?height conf_struct = let dialog = GWindow.dialog ~position:`CENTER ~modal: true ~title: title - ?height ?width + ~type_hint:`DIALOG + ?parent ?height ?width () in let tooltips = GData.tooltips () in @@ -807,3 +808,40 @@ let custom ?label box f expand = custom_expand = expand ; custom_framed = label ; } + +(* Copying lablgtk question_box + forbidding hiding *) + +let question_box ~title ~buttons ?(default=1) ?icon ?parent message = + let button_nb = ref 0 in + let window = GWindow.dialog ~position:`CENTER ~modal:true ?parent ~type_hint:`DIALOG ~title () in + let hbox = GPack.hbox ~border_width:10 ~packing:window#vbox#add () in + let bbox = window#action_area in + begin match icon with + None -> () + | Some i -> hbox#pack i#coerce ~padding:4 + end; + ignore (GMisc.label ~text: message ~packing: hbox#add ()); + (* the function called to create each button by iterating *) + let rec iter_buttons n = function + [] -> + () + | button_label :: q -> + let b = GButton.button ~label: button_label + ~packing:(bbox#pack ~expand:true ~padding:4) () + in + ignore (b#connect#clicked ~callback: + (fun () -> button_nb := n; window#destroy ())); + (* If it's the first button then give it the focus *) + if n = default then b#grab_default () else (); + + iter_buttons (n+1) q + in + iter_buttons 1 buttons; + ignore (window#connect#destroy ~callback: GMain.Main.quit); + window#set_position `CENTER; + window#show (); + GMain.Main.main (); + !button_nb + +let message_box ~title ?icon ?parent ?(ok="Ok") message = + ignore (question_box ?icon ?parent ~title message ~buttons:[ ok ]) diff --git a/ide/configwin_ihm.mli b/ide/configwin_ihm.mli index c867ad9127..772a0958ff 100644 --- a/ide/configwin_ihm.mli +++ b/ide/configwin_ihm.mli @@ -60,7 +60,17 @@ val edit : ?with_apply:bool -> ?apply:(unit -> unit) -> string -> + ?parent:GWindow.window -> ?width:int -> ?height:int -> configuration_structure list -> return_button + +val question_box : title:string -> + buttons:string list -> + ?default:int -> ?icon:#GObj.widget -> + ?parent:GWindow.window -> string -> int + +val message_box : + title:string -> ?icon:#GObj.widget -> + ?parent:GWindow.window -> ?ok:string -> string -> unit diff --git a/ide/coqide.ml b/ide/coqide.ml index a26f7d1b94..40b8d2f484 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -103,7 +103,8 @@ let make_coqtop_args fname = with | None -> "", base_args | Some proj -> - proj, coqtop_args_from_project (read_project_file proj) @ base_args + let warning_fn x = Feedback.msg_warning Pp.(str x) in + proj, coqtop_args_from_project (read_project_file ~warning_fn proj) @ base_args in let args = match fname with | None -> args @@ -112,7 +113,6 @@ let make_coqtop_args fname = else "-topfile"::fname::args in proj, args -;; (** Setting drag & drop on widgets *) @@ -190,8 +190,8 @@ let load_file ?(maycreate=false) f = let confirm_save ok = if ok then flash_info "Saved" else warning "Save Failed" -let select_and_save ~saveas ?filename sn = - let do_save = if saveas then sn.fileops#saveas else sn.fileops#save in +let select_and_save ?parent ~saveas ?filename sn = + let do_save = if saveas then sn.fileops#saveas ?parent else sn.fileops#save in let title = if saveas then "Save file as" else "Save file" in match select_file_for_save ~title ?filename () with |None -> false @@ -201,9 +201,9 @@ let select_and_save ~saveas ?filename sn = if ok then sn.tab_label#set_text (Filename.basename f); ok -let check_save ~saveas sn = +let check_save ?parent ~saveas sn = try match sn.fileops#filename with - |None -> select_and_save ~saveas sn + |None -> select_and_save ?parent ~saveas sn |Some f -> let ok = sn.fileops#save f in confirm_save ok; @@ -212,16 +212,17 @@ let check_save ~saveas sn = exception DontQuit -let check_quit saveall = +let check_quit ?parent saveall = (try save_pref () with _ -> flash_info "Cannot save preferences"); let is_modified sn = sn.buffer#modified in if List.exists is_modified notebook#pages then begin - let answ = GToolbox.question_box ~title:"Quit" + let answ = Configwin_ihm.question_box ~title:"Quit" ~buttons:["Save Named Buffers and Quit"; "Quit without Saving"; "Don't Quit"] ~default:0 ~icon:(warn_image ())#coerce + ?parent "There are unsaved buffers" in match answ with @@ -278,15 +279,15 @@ let load _ = | None -> () | Some f -> FileAux.load_file f -let save _ = on_current_term (FileAux.check_save ~saveas:false) +let save ?parent _ = on_current_term (FileAux.check_save ?parent ~saveas:false) -let saveas sn = +let saveas ?parent sn = try let filename = sn.fileops#filename in - ignore (FileAux.select_and_save ~saveas:true ?filename sn) + ignore (FileAux.select_and_save ?parent ~saveas:true ?filename sn) with _ -> warning "Save Failed" -let saveas = cb_on_current_term saveas +let saveas ?parent = cb_on_current_term (saveas ?parent) let saveall _ = List.iter @@ -297,33 +298,34 @@ let saveall _ = let () = Coq.save_all := saveall -let revert_all _ = +let revert_all ?parent _ = List.iter - (fun sn -> if sn.fileops#changed_on_disk then sn.fileops#revert) + (fun sn -> if sn.fileops#changed_on_disk then sn.fileops#revert ?parent ()) notebook#pages -let quit _ = - try FileAux.check_quit saveall; exit 0 +let quit ?parent _ = + try FileAux.check_quit ?parent saveall; exit 0 with FileAux.DontQuit -> () -let close_buffer sn = +let close_buffer ?parent sn = let do_remove () = notebook#remove_page notebook#current_page in if not sn.buffer#modified then do_remove () else - let answ = GToolbox.question_box ~title:"Close" + let answ = Configwin_ihm.question_box ~title:"Close" ~buttons:["Save Buffer and Close"; "Close without Saving"; "Don't Close"] ~default:0 ~icon:(warn_image ())#coerce + ?parent "This buffer has unsaved modifications" in match answ with - | 1 when FileAux.check_save ~saveas:true sn -> do_remove () + | 1 when FileAux.check_save ?parent ~saveas:true sn -> do_remove () | 2 -> do_remove () | _ -> () -let close_buffer = cb_on_current_term close_buffer +let close_buffer ?parent = cb_on_current_term (close_buffer ?parent) let export kind sn = match sn.fileops#filename with @@ -434,16 +436,16 @@ let coq_makefile sn = let coq_makefile = cb_on_current_term coq_makefile -let editor sn = +let editor ?parent sn = match sn.fileops#filename with |None -> warning "Call to external editor available only on named files" |Some f -> File.save (); let f = Filename.quote f in let cmd = Util.subst_command_placeholder cmd_editor#get f in - run_command ignore (fun _ -> sn.fileops#revert) cmd + run_command ignore (fun _ -> sn.fileops#revert ?parent ()) cmd -let editor = cb_on_current_term editor +let editor ?parent = cb_on_current_term (editor ?parent) let compile sn = File.save (); @@ -945,7 +947,7 @@ let build_ui () = try w#set_icon (Some (GdkPixbuf.from_file (MiscMenu.coq_icon ()))) with _ -> () in - let _ = w#event#connect#delete ~callback:(fun _ -> File.quit (); true) in + let _ = w#event#connect#delete ~callback:(fun _ -> File.quit ~parent:w (); true) in let _ = set_drag w#drag in let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in @@ -971,18 +973,18 @@ let build_ui () = item "File" ~label:"_File"; item "New" ~callback:File.newfile ~stock:`NEW; item "Open" ~callback:File.load ~stock:`OPEN; - item "Save" ~callback:File.save ~stock:`SAVE ~tooltip:"Save current buffer"; - item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:File.saveas; + item "Save" ~callback:(File.save ~parent:w) ~stock:`SAVE ~tooltip:"Save current buffer"; + item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:(File.saveas ~parent:w); item "Save all" ~label:"Sa_ve all" ~callback:File.saveall; item "Revert all buffers" ~label:"_Revert all buffers" - ~callback:File.revert_all ~stock:`REVERT_TO_SAVED; + ~callback:(File.revert_all ~parent:w) ~stock:`REVERT_TO_SAVED; item "Close buffer" ~label:"_Close buffer" ~stock:`CLOSE - ~callback:File.close_buffer ~tooltip:"Close current buffer"; + ~callback:(File.close_buffer ~parent:w) ~tooltip:"Close current buffer"; item "Print..." ~label:"_Print..." ~callback:File.print ~stock:`PRINT ~accel:"<Ctrl>p"; item "Rehighlight" ~label:"Reh_ighlight" ~accel:"<Ctrl>l" ~callback:File.highlight ~stock:`REFRESH; - item "Quit" ~stock:`QUIT ~callback:File.quit; + item "Quit" ~stock:`QUIT ~callback:(File.quit ~parent:w); ]; menu export_menu [ @@ -1013,14 +1015,12 @@ let build_ui () = item "Find Previous" ~label:"Find _Previous" ~stock:`GO_UP ~accel:"<Shift>F3" ~callback:(cb_on_current_term (fun t -> t.finder#find_backward ())); - item "Complete Word" ~label:"Complete Word" ~accel:"<Ctrl>slash" - ~callback:(fun _ -> ()); item "External editor" ~label:"External editor" ~stock:`EDIT - ~callback:External.editor; + ~callback:(External.editor ~parent:w); item "Preferences" ~accel:"<Ctrl>comma" ~stock:`PREFERENCES ~callback:(fun _ -> begin - try Preferences.configure ~apply:refresh_notebook_pos () + try Preferences.configure ~apply:refresh_notebook_pos w with _ -> flash_info "Cannot save preferences" end; reset_revert_timer ()); @@ -1309,8 +1309,8 @@ let build_ui () = (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); (* Showtime ! *) - w#show () - + w#show (); + w (** {2 Coqide main function } *) @@ -1325,7 +1325,7 @@ let make_scratch_buffer () = () let main files = - build_ui (); + let w = build_ui () in reset_revert_timer (); reset_autosave_timer (); (match files with @@ -1334,8 +1334,8 @@ let main files = notebook#goto_page 0; MiscMenu.initial_about (); on_current_term (fun t -> t.script#misc#grab_focus ()); - Minilib.log "End of Coqide.main" - + Minilib.log "End of Coqide.main"; + w (** {2 Argument parsing } *) @@ -1355,7 +1355,8 @@ let read_coqide_args argv = if project_files <> None then (output_string stderr "Error: multiple -f options"; exit 1); let d = CUnix.canonical_path_name (Filename.dirname file) in - let p = CoqProject_file.read_project_file file in + let warning_fn x = Format.eprintf "%s@\n%!" x in + let p = CoqProject_file.read_project_file ~warning_fn file in filter_coqtop coqtop (Some (d,p)) out args |"-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1 @@ -1391,9 +1392,9 @@ let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup; Sys.sigill; Sys.sigpipe; Sys.sigquit; Sys.sigusr1; Sys.sigusr2] -let set_signal_handlers () = +let set_signal_handlers ?parent () = try - Sys.set_signal Sys.sigint (Sys.Signal_handle File.quit); + Sys.set_signal Sys.sigint (Sys.Signal_handle (File.quit ?parent)); List.iter (fun i -> Sys.set_signal i (Sys.Signal_handle FileAux.crash_save)) signals_to_crash diff --git a/ide/coqide.mli b/ide/coqide.mli index 03e8545377..1d438ec381 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -22,7 +22,7 @@ val logfile : string option ref val read_coqide_args : string list -> string list (** Prepare the widgets, load the given files in tabs *) -val main : string list -> unit +val main : string list -> GWindow.window (** Function to save anything and kill all coqtops @return [false] if you're allowed to quit. *) @@ -37,7 +37,7 @@ val do_load : string -> unit (** Set coqide to perform a clean quit at Ctrl-C, while launching [crash_save] and exiting for others received signals *) -val set_signal_handlers : unit -> unit +val set_signal_handlers : ?parent:GWindow.window -> unit -> unit (** Emergency saving of opened files as "foo.v.crashcoqide", and exit (if the integer isn't 127). *) diff --git a/ide/coqide_main.ml b/ide/coqide_main.ml index 91e8be875a..21f513b8f4 100644 --- a/ide/coqide_main.ml +++ b/ide/coqide_main.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -let _ = Coqide.set_signal_handlers () let _ = GtkMain.Main.init () (* We handle Gtk warning messages ourselves : @@ -62,7 +61,8 @@ let () = let args = List.filter (fun x -> not (List.mem x files)) argl in Coq.check_connection args; Coqide.sup_args := args; - Coqide.main files; + let w = Coqide.main files in + Coqide.set_signal_handlers ~parent:w (); Coqide_os_specific.init (); try GMain.main (); diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 91c529932f..c994898a4f 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -60,7 +60,6 @@ let init () = \n <menuitem action='Find' />\ \n <menuitem action='Find Next' />\ \n <menuitem action='Find Previous' />\ -\n <menuitem action='Complete Word' />\ \n <separator />\ \n <menuitem action='External editor' />\ \n <separator />\ diff --git a/ide/fileOps.ml b/ide/fileOps.ml index 7acd2c37a9..e4c8942cf1 100644 --- a/ide/fileOps.ml +++ b/ide/fileOps.ml @@ -18,10 +18,10 @@ object method filename : string option method update_stats : unit method changed_on_disk : bool - method revert : unit + method revert : ?parent:GWindow.window -> unit -> unit method auto_save : unit method save : string -> bool - method saveas : string -> bool + method saveas : ?parent:GWindow.window -> string -> bool end class fileops (buffer:GText.buffer) _fn (reset_handler:unit->unit) = @@ -48,7 +48,7 @@ object(self) false |_ -> false - method revert = + method revert ?parent () = let do_revert f = push_info "Reverting buffer"; try @@ -72,13 +72,14 @@ object(self) | Some f -> if not buffer#modified then do_revert f else - let answ = GToolbox.question_box + let answ = Configwin_ihm.question_box ~title:"Modified buffer changed on disk" ~buttons:["Revert from File"; "Overwrite File"; "Disable Auto Revert"] ~default:0 ~icon:(stock_to_widget `DIALOG_WARNING) + ?parent "Some unsaved buffers changed on disk" in match answ with @@ -102,13 +103,14 @@ object(self) end else false - method saveas f = + method saveas ?parent f = if not (Sys.file_exists f) then self#save f else - let answ = GToolbox.question_box ~title:"File exists on disk" + let answ = Configwin_ihm.question_box ~title:"File exists on disk" ~buttons:["Overwrite"; "Cancel";] ~default:1 ~icon:(warn_image ())#coerce + ?parent ("File "^f^" already exists") in match answ with diff --git a/ide/fileOps.mli b/ide/fileOps.mli index 9a1f0cb738..44a19f9981 100644 --- a/ide/fileOps.mli +++ b/ide/fileOps.mli @@ -16,10 +16,10 @@ object method filename : string option method update_stats : unit method changed_on_disk : bool - method revert : unit + method revert : ?parent:GWindow.window -> unit -> unit method auto_save : unit method save : string -> bool - method saveas : string -> bool + method saveas : ?parent:GWindow.window -> string -> bool end class fileops : GText.buffer -> string option -> (unit -> unit) -> ops diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index 002722ace9..f2913b1d1d 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -153,13 +153,13 @@ let emacs = insert emacs "Emacs" [] [ i#forward_sentence_end, { s with move = None })); mkE ~mods:mM _a "a" "Move to beginning of sentence" (Motion(fun s i -> i#backward_sentence_start, { s with move = None })); - mkE _n "n" "Move to next line" ~alias:[[],_Down,"DOWN"] (Motion(fun s i -> + mkE _n "n" "Move to next line" (Motion(fun s i -> let orig_off = Option.default i#line_offset s.move in let i = i#forward_line in let new_off = min (i#chars_in_line - 1) orig_off in (if new_off > 0 then i#set_line_offset new_off else i), { s with move = Some orig_off })); - mkE _p "p" "Move to previous line" ~alias:[[],_Up,"UP"] (Motion(fun s i -> + mkE _p "p" "Move to previous line" (Motion(fun s i -> let orig_off = Option.default i#line_offset s.move in let i = i#backward_line in let new_off = min (i#chars_in_line - 1) orig_off in diff --git a/ide/preferences.ml b/ide/preferences.ml index 6dc922c225..045d650c1c 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -688,7 +688,7 @@ let pmodifiers ?(all = false) name p = modifiers name (str_to_mod_list p#get) -let configure ?(apply=(fun () -> ())) () = +let configure ?(apply=(fun () -> ())) parent = let cmd_coqtop = string ~f:(fun s -> cmd_coqtop#set (if s = "AUTO" then None else Some s)) @@ -1068,7 +1068,7 @@ let configure ?(apply=(fun () -> ())) () = (* Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string current.text_font); *) - let x = edit ~apply "Customizations" cmds in + let x = edit ~apply "Customizations" ~parent cmds in (* Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string current.text_font); *) diff --git a/ide/preferences.mli b/ide/preferences.mli index dd2976efc2..7ed6a40bdb 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -107,7 +107,7 @@ val diffs : string preference val save_pref : unit -> unit val load_pref : unit -> unit -val configure : ?apply:(unit -> unit) -> unit -> unit +val configure : ?apply:(unit -> unit) -> GWindow.window -> unit val stick : 'a preference -> (#GObj.widget as 'obj) -> ('a -> unit) -> unit diff --git a/interp/declare.ml b/interp/declare.ml index a9bfe8cabb..1e972d3e35 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -358,10 +358,6 @@ let inInductive : mutual_inductive_entry -> obj = let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = let id = Label.to_id label in - let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in - Recordops.declare_primitive_projection p; - (* ^ needs to happen before declaring the constant, otherwise - Heads gets confused. *) let univs = match univs with | Monomorphic_ind_entry _ -> (** Global constraints already defined through the inductive *) @@ -378,7 +374,10 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter Vars.subst_instance_constr u term, Vars.subst_instance_constr u types in let entry = definition_entry ~types ~univs term in - ignore(declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent)) + let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in + let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in + Recordops.declare_primitive_projection p cst + let declare_projections univs mind = let env = Global.env () in diff --git a/kernel/environ.ml b/kernel/environ.ml index f61dd0c101..019c0a6819 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -384,8 +384,26 @@ let set_engagement c env = (* Unsafe *) { env with env_stratification = { env.env_stratification with env_engagement = c } } +(* It's convenient to use [{flags with foo = bar}] so we're smart wrt to it. *) +let same_flags { + check_guarded; + check_universes; + conv_oracle; + share_reduction; + enable_VM; + enable_native_compiler; + } alt = + check_guarded == alt.check_guarded && + check_universes == alt.check_universes && + conv_oracle == alt.conv_oracle && + share_reduction == alt.share_reduction && + enable_VM == alt.enable_VM && + enable_native_compiler == alt.enable_native_compiler +[@warning "+9"] + let set_typing_flags c env = (* Unsafe *) - { env with env_typing_flags = c } + if same_flags env.env_typing_flags c then env + else { env with env_typing_flags = c } (* Global constants *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index df10398b2f..2464df799e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -192,7 +192,9 @@ let set_engagement c senv = engagement = Some c } let set_typing_flags c senv = - { senv with env = Environ.set_typing_flags c senv.env } + let env = Environ.set_typing_flags c senv.env in + if env == senv.env then senv + else { senv with env } let set_share_reduction b senv = let flags = Environ.typing_flags senv.env in diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 9ff51fca55..9083156745 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -942,34 +942,36 @@ let check_eq_instances g t1 t2 = (** Pretty-printing *) +let pr_umap sep pr map = + let cmp (u,_) (v,_) = Level.compare u v in + Pp.prlist_with_sep sep pr (List.sort cmp (UMap.bindings map)) + let pr_arc prl = function | _, Canonical {univ=u; ltle; _} -> if UMap.is_empty ltle then mt () else prl u ++ str " " ++ v 0 - (pr_sequence (fun (v, strict) -> + (pr_umap Pp.spc (fun (v, strict) -> (if strict then str "< " else str "<= ") ++ prl v) - (UMap.bindings ltle)) ++ + ltle) ++ fnl () | u, Equiv v -> prl u ++ str " = " ++ prl v ++ fnl () let pr_universes prl g = - let graph = UMap.fold (fun u a l -> (u,a)::l) g.entries [] in - prlist (pr_arc prl) graph + pr_umap mt (pr_arc prl) g.entries (* Dumping constraints to a file *) let dump_universes output g = let dump_arc u = function | Canonical {univ=u; ltle; _} -> - let u_str = Level.to_string u in UMap.iter (fun v strict -> let typ = if strict then Lt else Le in - output typ u_str (Level.to_string v)) ltle; + output typ u v) ltle; | Equiv v -> - output Eq (Level.to_string u) (Level.to_string v) + output Eq u v in UMap.iter dump_arc g.entries diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 4336a22b8c..a2cc5b3116 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -86,7 +86,7 @@ val check_subtype : AUContext.t check_function (** {6 Dumping to a file } *) val dump_universes : - (constraint_type -> string -> string -> unit) -> t -> unit + (constraint_type -> Level.t -> Level.t -> unit) -> t -> unit (** {6 Debugging} *) val check_universes_invariants : t -> unit diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml index 7395654022..868042303d 100644 --- a/lib/coqProject_file.ml +++ b/lib/coqProject_file.ml @@ -12,10 +12,6 @@ ideally we would like to make this independent so it can be bootstrapped. *) -(* Note the problem with the error invokation below calling exit... *) -(* let error msg = Feedback.msg_error msg *) -let warning msg = Feedback.msg_warning Pp.(str msg) - type arg_source = CmdLine | ProjectFile type 'a sourced = { thing : 'a; source : arg_source } @@ -147,7 +143,7 @@ let exists_dir dir = try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false -let process_cmd_line orig_dir proj args = +let process_cmd_line ~warning_fn orig_dir proj args = let parsing_project_file = ref (proj.project_file <> None) in let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in let orig_dir = (* avoids turning foo.v in ./foo.v *) @@ -170,7 +166,7 @@ let process_cmd_line orig_dir proj args = | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt = true } r | "-install" :: d :: r -> if proj.install_kind <> None then - (warning "-install set more than once.@\n%!"); + (warning_fn "-install set more than once."); let install = match d with | "user" -> UserInstall | "none" -> NoInstall @@ -197,7 +193,7 @@ let process_cmd_line orig_dir proj args = let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in let () = match proj.project_file with | None -> () - | Some _ -> warning "Multiple project files are deprecated.@\n%!" + | Some _ -> warning_fn "Multiple project files are deprecated." in parsing_project_file := true; let proj = aux { proj with project_file = Some file } (parse file) in @@ -236,11 +232,11 @@ let process_cmd_line orig_dir proj args = (******************************* API ************************************) -let cmdline_args_to_project ~curdir args = - process_cmd_line curdir (mk_project None None None true) args +let cmdline_args_to_project ~warning_fn ~curdir args = + process_cmd_line ~warning_fn curdir (mk_project None None None true) args -let read_project_file f = - process_cmd_line (Filename.dirname f) +let read_project_file ~warning_fn f = + process_cmd_line ~warning_fn (Filename.dirname f) (mk_project (Some f) None (Some NoInstall) true) (parse f) let rec find_project_file ~from ~projfile_name = diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 2a6a09a9a0..20b276ce8c 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -51,8 +51,8 @@ and install = | TraditionalInstall | UserInstall -val cmdline_args_to_project : curdir:string -> string list -> project -val read_project_file : string -> project +val cmdline_args_to_project : warning_fn:(string -> unit) -> curdir:string -> string list -> project +val read_project_file : warning_fn:(string -> unit) -> string -> project val coqtop_args_from_project : project -> string list val find_project_file : from:string -> projfile_name:string -> string option diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 85fb0c73c9..70e5ab38bc 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -48,7 +48,6 @@ let with_delayed_uconstr ist c tac = let flags = { Pretyping.use_typeclasses = false; solve_unification_constraints = true; - use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } in @@ -343,7 +342,6 @@ open Vars let constr_flags () = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics (); - Pretyping.use_hook = Pfedit.solve_by_implicit_tactic (); Pretyping.fail_evar = false; Pretyping.expand_evars = true } @@ -571,44 +569,6 @@ VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF { add_transitivity_lemma false t } END -{ - -let cache_implicit_tactic (_,tac) = match tac with - | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac) - | None -> Pfedit.clear_implicit_tactic () - -let subst_implicit_tactic (subst,tac) = - Option.map (Tacsubst.subst_tactic subst) tac - -let inImplicitTactic : glob_tactic_expr option -> obj = - declare_object {(default_object "IMPLICIT-TACTIC") with - open_function = (fun i o -> if Int.equal i 1 then cache_implicit_tactic o); - cache_function = cache_implicit_tactic; - subst_function = subst_implicit_tactic; - classify_function = (fun o -> Dispose)} - -let warn_deprecated_implicit_tactic = - CWarnings.create ~name:"deprecated-implicit-tactic" ~category:"deprecated" - (fun () -> strbrk "Implicit tactics are deprecated") - -let declare_implicit_tactic tac = - let () = warn_deprecated_implicit_tactic () in - Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac))) - -let clear_implicit_tactic () = - let () = warn_deprecated_implicit_tactic () in - Lib.add_anonymous_leaf (inImplicitTactic None) - -} - -VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF -| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> { declare_implicit_tactic tac } -| [ "Clear" "Implicit" "Tactic" ] -> { clear_implicit_tactic () } -END - - - - (**********************************************************************) (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as defined by Conor McBride *) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 5af393a3e5..7be8f67616 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -55,7 +55,6 @@ let eval_uconstrs ist cs = let flags = { Pretyping.use_typeclasses = false; solve_unification_constraints = true; - use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } in diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 2a046a3e65..5bfb0f79fb 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -543,7 +543,6 @@ let interp_gen kind ist pattern_mode flags env sigma c = let constr_flags () = { use_typeclasses = true; solve_unification_constraints = true; - use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = true; expand_evars = true } @@ -558,21 +557,18 @@ let interp_type = interp_constr_gen IsType let open_constr_use_classes_flags () = { use_typeclasses = true; solve_unification_constraints = true; - use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } let open_constr_no_classes_flags () = { use_typeclasses = false; solve_unification_constraints = true; - use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } let pure_open_constr_flags = { use_typeclasses = false; solve_unification_constraints = true; - use_hook = None; fail_evar = false; expand_evars = false } @@ -987,7 +983,7 @@ let rec read_match_rule lfun ist env sigma = function | [] -> [] (* Fully evaluate an untyped constr *) -let type_uconstr ?(flags = {(constr_flags ()) with use_hook = None }) +let type_uconstr ?(flags = (constr_flags ())) ?(expected_type = WithoutTypeConstraint) ist c = begin fun env sigma -> let { closure; term } = c in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index be8f3603e4..ddfd4c101f 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -242,7 +242,6 @@ let interp_refine ist gl rc = let flags = { Pretyping.use_typeclasses = true; solve_unification_constraints = true; - use_hook = None; fail_evar = false; expand_evars = true } in diff --git a/pretyping/heads.ml b/pretyping/heads.ml index a3e4eb8971..e533930267 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -26,9 +26,8 @@ open Context.Named.Declaration the evaluation of [phi(0)] and the head of [h] is declared unknown). *) type rigid_head_kind = -| RigidParameter of Constant.t (* a Const without body *) -| RigidVar of variable (* a Var without body *) -| RigidType (* an inductive, a product or a sort *) +| RigidParameter of Constant.t (* a Const without body. Module substitution may instantiate it with something else. *) +| RigidOther (* a Var without body, inductive, product, sort, projection *) type head_approximation = | RigidHead of rigid_head_kind @@ -77,7 +76,7 @@ let kind_of_head env t = str ".")) | Construct _ | CoFix _ -> if b then NotImmediatelyComputableHead else ConstructorHead - | Sort _ | Ind _ | Prod _ -> RigidHead RigidType + | Sort _ | Ind _ | Prod _ -> RigidHead RigidOther | Cast (c,_,_) -> aux k l c b | Lambda (_,_,c) -> begin match l with @@ -89,9 +88,7 @@ let kind_of_head env t = | LetIn _ -> assert false | Meta _ | Evar _ -> NotImmediatelyComputableHead | App (c,al) -> aux k (Array.to_list al @ l) c b - | Proj (p,c) -> - (try on_subterm k (c :: l) b (constant_head (Projection.constant p)) - with Not_found -> assert false) + | Proj (p,c) -> RigidHead RigidOther | Case (_,_,c,_) -> aux k [] c true | Fix ((i,j),_) -> @@ -124,22 +121,16 @@ let kind_of_head env t = (* FIXME: maybe change interface here *) let compute_head = function | EvalConstRef cst -> - let env = Global.env() in - let cb = Environ.lookup_constant cst env in - let is_Def = function Declarations.Def _ -> true | _ -> false in - let body = - if not (Recordops.is_primitive_projection cst) && is_Def cb.Declarations.const_body - then Global.body_of_constant cst else None - in - (match body with - | None -> RigidHead (RigidParameter cst) - | Some (c, _) -> kind_of_head env c) + let env = Global.env() in + let body = Environ.constant_opt_value_in env (cst,Univ.Instance.empty) in + (match body with + | None -> RigidHead (RigidParameter cst) + | Some c -> kind_of_head env c) | EvalVarRef id -> (match Global.lookup_named id with | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> kind_of_head (Global.env()) c - | _ -> - RigidHead (RigidVar id)) + | _ -> RigidHead RigidOther) let is_rigid env t = match kind_of_head env t with diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index cba1533da5..8c57fc2375 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -193,7 +193,6 @@ type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr type inference_flags = { use_typeclasses : bool; solve_unification_constraints : bool; - use_hook : inference_hook option; fail_evar : bool; expand_evars : bool } @@ -247,14 +246,14 @@ let apply_typeclasses env sigma frozen fail_evar = else sigma in sigma -let apply_inference_hook hook sigma frozen = match frozen with +let apply_inference_hook hook env sigma frozen = match frozen with | FrozenId _ -> sigma | FrozenProgress (lazy (_, pending)) -> Evar.Set.fold (fun evk sigma -> if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then try - let sigma, c = hook sigma evk in + let sigma, c = hook env sigma evk in Evd.define evk c sigma with Exit -> sigma @@ -307,16 +306,16 @@ let check_evars_are_solved env sigma frozen = (* Try typeclasses, hooks, unification heuristics ... *) -let solve_remaining_evars flags env sigma init_sigma = +let solve_remaining_evars ?hook flags env sigma init_sigma = let frozen = frozen_and_pending_holes (init_sigma, sigma) in let sigma = if flags.use_typeclasses then apply_typeclasses env sigma frozen false else sigma in - let sigma = if Option.has_some flags.use_hook - then apply_inference_hook (Option.get flags.use_hook env) sigma frozen - else sigma + let sigma = match hook with + | None -> sigma + | Some hook -> apply_inference_hook hook env sigma frozen in let sigma = if flags.solve_unification_constraints then apply_heuristics env sigma false @@ -1075,14 +1074,12 @@ let ise_pretype_gen flags env sigma lvar kind c = let default_inference_flags fail = { use_typeclasses = true; solve_unification_constraints = true; - use_hook = None; fail_evar = fail; expand_evars = true } let no_classes_no_fail_inference_flags = { use_typeclasses = false; solve_unification_constraints = true; - use_hook = None; fail_evar = false; expand_evars = true } diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 0f95d27528..2eaa77b822 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -35,7 +35,6 @@ type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr type inference_flags = { use_typeclasses : bool; solve_unification_constraints : bool; - use_hook : inference_hook option; fail_evar : bool; expand_evars : bool } @@ -95,7 +94,7 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> with candidate and no other conversion problems that the one in [pending], however, it can contain more evars than the pending ones. *) -val solve_remaining_evars : inference_flags -> +val solve_remaining_evars : ?hook:inference_hook -> inference_flags -> env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map (** Checking evars and pending conversion problems are all solved, diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 4faa753dfb..fe9b69dbbc 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -106,16 +106,16 @@ let find_projection = function let prim_table = Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs" -let load_prim i (_,p) = - prim_table := Cmap_env.add (Projection.Repr.constant p) p !prim_table +let load_prim i (_,(p,c)) = + prim_table := Cmap_env.add c p !prim_table let cache_prim p = load_prim 1 p -let subst_prim (subst,p) = subst_proj_repr subst p +let subst_prim (subst,(p,c)) = subst_proj_repr subst p, subst_constant subst c -let discharge_prim (_,p) = Some (Lib.discharge_proj_repr p) +let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) -let inPrim : Projection.Repr.t -> obj = +let inPrim : (Projection.Repr.t * Constant.t) -> obj = declare_object { (default_object "PRIMPROJS") with cache_function = cache_prim ; @@ -124,7 +124,7 @@ let inPrim : Projection.Repr.t -> obj = classify_function = (fun x -> Substitute x); discharge_function = discharge_prim } -let declare_primitive_projection p = Lib.add_anonymous_leaf (inPrim p) +let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) let is_primitive_projection c = Cmap_env.mem c !prim_table diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 415b964168..3e43372b65 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -45,7 +45,7 @@ val find_projection_nparams : GlobRef.t -> int val find_projection : GlobRef.t -> struc_typ (** Sets up the mapping from constants to primitive projections *) -val declare_primitive_projection : Projection.Repr.t -> unit +val declare_primitive_projection : Projection.Repr.t -> Constant.t -> unit val is_primitive_projection : Constant.t -> bool diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index c80f370fdc..cb71f09826 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -53,7 +53,6 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = let flags = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = true; - Pretyping.use_hook = None; Pretyping.fail_evar = false; Pretyping.expand_evars = true } in try Pretyping.understand_ltac flags diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index e6507332b1..7b55941874 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -227,36 +227,3 @@ let refine_by_tactic env sigma ty tac = this hack will work in most cases. *) let ans = Safe_typing.inline_private_constants_in_constr env ans neff in ans, sigma - -(**********************************************************************) -(* Support for resolution of evars in tactic interpretation, including - resolution by application of tactics *) - -let implicit_tactic = Summary.ref None ~name:"implicit-tactic" - -let declare_implicit_tactic tac = implicit_tactic := Some tac - -let clear_implicit_tactic () = implicit_tactic := None - -let apply_implicit_tactic tac = (); fun env sigma evk -> - let evi = Evd.find_undefined sigma evk in - match snd (evar_source evk sigma) with - | (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) - when - Context.Named.equal Constr.equal (Environ.named_context_of_val evi.evar_hyps) - (Environ.named_context env) -> - let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in - (try - let c = Evarutil.nf_evars_universes sigma (EConstr.Unsafe.to_constr evi.evar_concl) in - let c = EConstr.of_constr c in - if Evarutil.has_undefined_evars sigma c then raise Exit; - let (ans, _, ctx) = - build_by_tactic env (Evd.evar_universe_context sigma) c tac in - let sigma = Evd.set_universe_context sigma ctx in - sigma, EConstr.of_constr ans - with e when Logic.catchable_exception e -> raise Exit) - | _ -> raise Exit - -let solve_by_implicit_tactic () = match !implicit_tactic with -| None -> None -| Some tac -> Some (apply_implicit_tactic tac) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 5feb5bd645..50ce267c81 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -116,13 +116,3 @@ val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.ta evars solved by side-effects are NOT purged, so that unexpected failures may occur. Ideally all code using this function should be rewritten in the monad. *) - -(** Declare the default tactic to fill implicit arguments *) - -val declare_implicit_tactic : unit Proofview.tactic -> unit - -(** To remove the default tactic *) -val clear_implicit_tactic : unit -> unit - -(* Raise Exit if cannot solve *) -val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1646906daa..03ad1b4c4f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1152,7 +1152,6 @@ let rec intros_move = function let tactic_infer_flags with_evar = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = true; - Pretyping.use_hook = Pfedit.solve_by_implicit_tactic (); Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true } diff --git a/test-suite/output/PrintUnivsSubgraph.out b/test-suite/output/PrintUnivsSubgraph.out new file mode 100644 index 0000000000..c42e15e4e8 --- /dev/null +++ b/test-suite/output/PrintUnivsSubgraph.out @@ -0,0 +1,5 @@ +Prop < Set +Set < i + < j +i < j + diff --git a/test-suite/output/PrintUnivsSubgraph.v b/test-suite/output/PrintUnivsSubgraph.v new file mode 100644 index 0000000000..ec9cf44d4f --- /dev/null +++ b/test-suite/output/PrintUnivsSubgraph.v @@ -0,0 +1,9 @@ + +Universes i j k l. + +Definition foo : Type@{j} := Type@{i}. + +Definition baz : Type@{k} := Type@{l}. + +Print Universes Subgraph(i j). +(* should print [i < j], not [l < k] (and not prelude universes) *) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ca5a232edb..8560bac786 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -396,8 +396,9 @@ let _ = | "-destination-of" :: tgt :: rest -> Some tgt, rest | _ -> None, args in - let project = - try cmdline_args_to_project ~curdir:Filename.current_dir_name args + let project = + let warning_fn x = Format.eprintf "%s@\n%!" x in + try cmdline_args_to_project ~warning_fn ~curdir:Filename.current_dir_name args with Parsing_error s -> prerr_endline s; usage_coq_makefile () in if only_destination <> None then begin diff --git a/tools/coqdep.ml b/tools/coqdep.ml index ba88069be9..226a19678f 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -473,7 +473,8 @@ let add_r_include path l = add_rec_dir_import add_known path (split_period l) let treat_coqproject f = let open CoqProject_file in let iter_sourced f = List.iter (fun {thing} -> f thing) in - let project = read_project_file f in + let warning_fn x = coqdep_warning "%s" x in + let project = read_project_file ~warning_fn f in iter_sourced (fun { path } -> add_caml_dir path) project.ml_includes; iter_sourced (fun ({ path }, l) -> add_q_include path l) project.q_includes; iter_sourced (fun ({ path }, l) -> add_r_include path l) project.r_includes; diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 1d0a5ab0a3..960e74827a 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -989,8 +989,9 @@ GRAMMAR EXTEND Gram | IDENT "Scope"; s = IDENT -> { PrintScope s } | IDENT "Visibility"; s = OPT IDENT -> { PrintVisibility s } | IDENT "Implicit"; qid = smart_global -> { PrintImplicit qid } - | IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (false, fopt) } - | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (true, fopt) } + | b = [ IDENT "Sorted" -> { true } | -> { false } ]; IDENT "Universes"; + g = OPT printunivs_subgraph; fopt = OPT ne_string -> + { PrintUniverses (b, g, fopt) } | IDENT "Assumptions"; qid = smart_global -> { PrintAssumptions (false, false, qid) } | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, false, qid) } | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (false, true, qid) } @@ -1000,6 +1001,9 @@ GRAMMAR EXTEND Gram | IDENT "Registered" -> { PrintRegistered } ] ] ; + printunivs_subgraph: + [ [ IDENT "Subgraph"; "("; l = LIST0 reference; ")" -> { l } ] ] + ; class_rawexpr: [ [ IDENT "Funclass" -> { FunClass } | IDENT "Sortclass" -> { SortClass } diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 3b041b7065..d537436c6b 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -418,8 +418,8 @@ let start_proof_com ?inference_hook kind thms hook = let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in let flags = all_and_fail_flags in - let flags = { flags with use_hook = inference_hook } in - let evd = solve_remaining_evars flags env evd Evd.empty in + let hook = inference_hook in + let evd = solve_remaining_evars ?hook flags env evd Evd.empty in let ids = List.map RelDecl.get_name ctx in check_name_freshness (pi1 kind) id; (* XXX: The nf_evar is critical !! *) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 1c1faca599..f65fae60ee 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -492,12 +492,13 @@ open Pputils keyword "Print Hint *" | PrintHintDbName s -> keyword "Print HintDb" ++ spc () ++ str s - | PrintUniverses (b, fopt) -> + | PrintUniverses (b, g, fopt) -> let cmd = if b then "Print Sorted Universes" else "Print Universes" in - keyword cmd ++ pr_opt str fopt + let pr_subgraph = prlist_with_sep spc pr_qualid in + keyword cmd ++ pr_opt pr_subgraph g ++ pr_opt str fopt | PrintName (qid,udecl) -> keyword "Print" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list udecl | PrintModuleType qid -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1fab35b650..7a76fb9560 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -319,7 +319,7 @@ let print_registered () = hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ()) -let dump_universes_gen g s = +let dump_universes_gen prl g s = let output = open_out s in let output_constraint, close = if Filename.check_suffix s ".dot" || Filename.check_suffix s ".gv" then begin @@ -344,10 +344,12 @@ let dump_universes_gen g s = | Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=" - in Printf.fprintf output "%s %s %s ;\n" left kind right + in + Printf.fprintf output "%s %s %s ;\n" left kind right end, (fun () -> close_out output) end in + let output_constraint k l r = output_constraint k (prl l) (prl r) in try UGraph.dump_universes output_constraint g; close (); @@ -357,6 +359,36 @@ let dump_universes_gen g s = close (); iraise reraise +let universe_subgraph ?loc g univ = + let open Univ in + let sigma = Evd.from_env (Global.env()) in + let univs_of q = + let q = Glob_term.(GType (UNamed q)) in + (* this function has a nice error message for not found univs *) + LSet.singleton (Pretyping.interp_known_glob_level ?loc sigma q) + in + let univs = List.fold_left (fun univs q -> LSet.union univs (univs_of q)) LSet.empty g in + let csts = UGraph.constraints_for ~kept:(LSet.add Level.prop (LSet.add Level.set univs)) univ in + let univ = LSet.fold UGraph.add_universe_unconstrained univs UGraph.initial_universes in + UGraph.merge_constraints csts univ + +let print_universes ?loc ~sort ~subgraph dst = + let univ = Global.universes () in + let univ = match subgraph with + | None -> univ + | Some g -> universe_subgraph ?loc g univ + in + let univ = if sort then UGraph.sort_universes univ else univ in + let pr_remaining = + if Global.is_joined_environment () then mt () + else str"There may remain asynchronous universe constraints" + in + let prl = UnivNames.pr_with_global_universes in + begin match dst with + | None -> UGraph.pr_universes prl univ ++ pr_remaining + | Some s -> dump_universes_gen (fun u -> Pp.string_of_ppcmds (prl u)) univ s + end + (*********************) (* "Locate" commands *) @@ -1826,17 +1858,7 @@ let vernac_print ~atts env sigma = | PrintCoercionPaths (cls,clt) -> Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt) | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma - | PrintUniverses (b, dst) -> - let univ = Global.universes () in - let univ = if b then UGraph.sort_universes univ else univ in - let pr_remaining = - if Global.is_joined_environment () then mt () - else str"There may remain asynchronous universe constraints" - in - begin match dst with - | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining - | Some s -> dump_universes_gen univ s - end + | PrintUniverses (sort, subgraph, dst) -> print_universes ~sort ~subgraph dst | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r) | PrintHintGoal -> Hints.pr_applicable_hint () | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 594e9eca48..180d763946 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -45,7 +45,7 @@ type printable = | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintCanonicalConversions - | PrintUniverses of bool * string option + | PrintUniverses of bool * qualid list option * string option | PrintHint of qualid or_by_notation | PrintHintGoal | PrintHintDbName of string |