From fd3bde66bc32ba70435aaad3f83d0b58c846af55 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 7 Dec 2018 23:15:26 +0100 Subject: [tactics] Remove dependency of abstract on global proof state. In order to do so we place the polymorphic status and name in the read-only part of the monad. Note the added comments, as well as the fact that almost no part of tactics depends on `proofs` nor `interp`, thus they should be placed just after pretyping. Gaëtan Gilbert noted that ideally, abstract should not depend on the polymorphic status, should we be able to defer closing of the constant, however this will require significant effort. Also, we may deprecate nameless abstract, thus rending both of the changes this PR need unnecessary. --- dev/ci/ci-fiat-parsers.sh | 9 --------- dev/ci/ci-fiat_parsers.sh | 9 +++++++++ .../user-overlays/06914-maximedenes-primitive-integers.sh | 9 --------- dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh | 6 ------ dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh | 6 ------ dev/ci/user-overlays/09172-ejgallego-proof_rework.sh | 9 --------- .../user-overlays/09173-ejgallego-proofview+proof_info.sh | 9 +++++++++ dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh | 6 ------ dev/ci/user-overlays/09263-maximedenes-parsing-state.sh | 12 ------------ dev/ci/user-overlays/09410-maximedenes-thread-program.sh | 13 ------------- 10 files changed, 18 insertions(+), 70 deletions(-) delete mode 100755 dev/ci/ci-fiat-parsers.sh create mode 100755 dev/ci/ci-fiat_parsers.sh delete mode 100644 dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh delete mode 100644 dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh delete mode 100644 dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh delete mode 100644 dev/ci/user-overlays/09172-ejgallego-proof_rework.sh create mode 100644 dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh delete mode 100644 dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh delete mode 100644 dev/ci/user-overlays/09263-maximedenes-parsing-state.sh delete mode 100644 dev/ci/user-overlays/09410-maximedenes-thread-program.sh (limited to 'dev') diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh deleted file mode 100755 index ac74ebf667..0000000000 --- a/dev/ci/ci-fiat-parsers.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -FORCE_GIT=1 -git_download fiat_parsers - -( cd "${CI_BUILD_DIR}/fiat_parsers" && make parsers parsers-examples && make fiat-core ) diff --git a/dev/ci/ci-fiat_parsers.sh b/dev/ci/ci-fiat_parsers.sh new file mode 100755 index 0000000000..ac74ebf667 --- /dev/null +++ b/dev/ci/ci-fiat_parsers.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download fiat_parsers + +( cd "${CI_BUILD_DIR}/fiat_parsers" && make parsers parsers-examples && make fiat-core ) diff --git a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh deleted file mode 100644 index 6e89741e29..0000000000 --- a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6914" ] || [ "$CI_BRANCH" = "primitive-bool-list" ]; then - - bignums_CI_REF=primitive-integers - bignums_CI_GITURL=https://github.com/vbgl/bignums - - mtac2_CI_REF=primitive-integers - mtac2_CI_GITURL=https://github.com/vbgl/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh deleted file mode 100644 index 2df8affd14..0000000000 --- a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then - - elpi_CI_REF=ltac+remove_aliases - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh deleted file mode 100644 index f2a113b118..0000000000 --- a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9150" ] || [ "$CI_BRANCH" = "build+warn_50" ]; then - - mtac2_CI_REF=build+warn_50 - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh deleted file mode 100644 index f532fdfc52..0000000000 --- a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then - - ltac2_CI_REF=proof_rework - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - mtac2_CI_REF=proof_rework - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh new file mode 100644 index 0000000000..23eb24c304 --- /dev/null +++ b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9173" ] || [ "$CI_BRANCH" = "proofview+proof_info" ]; then + + ltac2_CI_REF=proofview+proof_info + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + fiat_parsers_CI_REF=proofview+proof_info + fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat + +fi diff --git a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh deleted file mode 100644 index efcdd2e97f..0000000000 --- a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9220" ] || [ "$CI_BRANCH" = "stm-shallow-logic" ]; then - - paramcoq_CI_REF=stm-shallow-logic - paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq - -fi diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh deleted file mode 100644 index ebd1b524da..0000000000 --- a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9263" ] || [ "$CI_BRANCH" = "parsing-state" ]; then - - mtac2_CI_REF=proof-mode - mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2 - - ltac2_CI_REF=proof-mode - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - equations_CI_REF=proof-mode - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/09410-maximedenes-thread-program.sh b/dev/ci/user-overlays/09410-maximedenes-thread-program.sh deleted file mode 100644 index 985c2db74e..0000000000 --- a/dev/ci/user-overlays/09410-maximedenes-thread-program.sh +++ /dev/null @@ -1,13 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9410" ] || [ "$CI_BRANCH" = "thread-program" ]; then - - math_classes_CI_REF=program-mode-flag - math_classes_CI_GITURL=https://github.com/maximedenes/math-classes - - ltac2_CI_REF=program-mode-flag - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - - equations_CI_REF=thread-program - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -fi -- cgit v1.2.3