aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore1
-rw-r--r--META.coq72
-rw-r--r--Makefile.install5
-rw-r--r--configure.ml2
-rwxr-xr-xdev/ci/ci-color.sh9
-rw-r--r--dev/ci/ci-common.sh24
-rwxr-xr-xdev/ci/ci-compcert.sh7
-rwxr-xr-xdev/ci/ci-coquelicot.sh12
-rwxr-xr-xdev/ci/ci-cpdt.sh2
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh11
-rwxr-xr-xdev/ci/ci-fiat-parsers.sh8
-rwxr-xr-xdev/ci/ci-flocq.sh11
-rwxr-xr-xdev/ci/ci-geocoq.sh8
-rwxr-xr-xdev/ci/ci-hott.sh10
-rwxr-xr-xdev/ci/ci-iris-coq.sh21
-rwxr-xr-xdev/ci/ci-math-classes.sh24
-rwxr-xr-xdev/ci/ci-math-comp.sh8
-rwxr-xr-xdev/ci/ci-metacoq.sh22
-rwxr-xr-xdev/ci/ci-sf.sh2
-rwxr-xr-xdev/ci/ci-template.sh12
-rwxr-xr-xdev/ci/ci-tlc.sh10
-rwxr-xr-xdev/ci/ci-unimath.sh7
-rw-r--r--dev/core.dbg2
-rw-r--r--proofs/pfedit.ml7
24 files changed, 186 insertions, 111 deletions
diff --git a/.gitignore b/.gitignore
index 35cdf9b4e8..64c49b008c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -43,6 +43,7 @@ TAGS
.DS_Store
.pc
bin/
+_build_ci
_build
myocamlbuild_config.ml
config/Makefile
diff --git a/META.coq b/META.coq
index d83dab23d1..83134d4a08 100644
--- a/META.coq
+++ b/META.coq
@@ -1,5 +1,15 @@
+# TODO: Move to META.in once coq_makefile2 is merged.
+# We need to reuse:
+# - The variable substitution mechanism.
+# - Sourcing of "coq_install_path" and "coq_version" variables.
+#
+# With this rules, we would have:
+# version = ${coq_version}
+# and
+# linkopts(byte) = "-dllpath ${coq_install_path}/kernel/byterun/ -dllib -lcoqrun"
+
description = "The Coq Proof Assistant Plugin API"
-version = "8.6"
+version = "8.7"
directory = ""
requires = "camlp5"
@@ -7,7 +17,7 @@ requires = "camlp5"
package "config" (
description = "Coq Configuration Variables"
- version = "8.6"
+ version = "8.7"
directory = "config"
@@ -16,7 +26,7 @@ package "config" (
package "lib" (
description = "Base Coq Library"
- version = "8.6"
+ version = "8.7"
directory = "lib"
@@ -33,22 +43,16 @@ package "lib" (
package "vm" (
description = "Coq VM"
+ version = "8.7"
- version = "8.6"
-
-# EJGA FIXME: Unfortunately dllpath is dependent on the type of Coq
-# install. In a local one we'll want kernel/byterun, in a non-local
-# one we want to set it to coqlib. We should thus generate this file
-# at configure time, but let's hear for some more feedback from
-# experts.
+ directory = "kernel/byterun"
-# Enable for local native & byte builds
-# directory = "kernel/byterun"
+# We should generate this file at configure time for local byte builds
+# to work properly.
-# Enable for local byte builds and set up properly
-# linkopts(byte) = "-dllpath /path/to/coq/kernel/byterun/ -dllib -lcoqrun"
+# Enable this setting for local byte builds, disabling the one below.
+# linkopts(byte) = "-dllpath path_to_coq/kernel/byterun/ -dllib -lcoqrun"
-# Disable for local byte builds
linkopts(byte) = "-dllib -lcoqrun"
linkopts(native) = "-cclib -lcoqrun"
@@ -57,7 +61,7 @@ package "vm" (
package "kernel" (
description = "Coq's Kernel"
- version = "8.6"
+ version = "8.7"
directory = "kernel"
@@ -71,7 +75,7 @@ package "kernel" (
package "library" (
description = "Coq Libraries (vo) support"
- version = "8.6"
+ version = "8.7"
requires = "coq.kernel"
@@ -85,7 +89,7 @@ package "library" (
package "intf" (
description = "Coq Public Data Types"
- version = "8.6"
+ version = "8.7"
requires = "coq.library"
@@ -96,7 +100,7 @@ package "intf" (
package "engine" (
description = "Coq Tactic Engine"
- version = "8.6"
+ version = "8.7"
requires = "coq.library"
directory = "engine"
@@ -109,7 +113,7 @@ package "engine" (
package "pretyping" (
description = "Coq Pretyper"
- version = "8.6"
+ version = "8.7"
requires = "coq.engine"
directory = "pretyping"
@@ -122,7 +126,7 @@ package "pretyping" (
package "interp" (
description = "Coq Term Interpretation"
- version = "8.6"
+ version = "8.7"
requires = "coq.pretyping"
directory = "interp"
@@ -135,7 +139,7 @@ package "interp" (
package "grammar" (
description = "Coq Base Grammar"
- version = "8.6"
+ version = "8.7"
requires = "coq.interp"
directory = "grammar"
@@ -147,7 +151,7 @@ package "grammar" (
package "proofs" (
description = "Coq Proof Engine"
- version = "8.6"
+ version = "8.7"
requires = "coq.interp"
directory = "proofs"
@@ -160,7 +164,7 @@ package "proofs" (
package "parsing" (
description = "Coq Parsing Engine"
- version = "8.6"
+ version = "8.7"
requires = "coq.proofs"
directory = "parsing"
@@ -173,7 +177,7 @@ package "parsing" (
package "printing" (
description = "Coq Printing Engine"
- version = "8.6"
+ version = "8.7"
requires = "coq.parsing"
directory = "printing"
@@ -186,7 +190,7 @@ package "printing" (
package "tactics" (
description = "Coq Basic Tactics"
- version = "8.6"
+ version = "8.7"
requires = "coq.printing"
directory = "tactics"
@@ -199,7 +203,7 @@ package "tactics" (
package "vernac" (
description = "Coq Vernacular Interpreter"
- version = "8.6"
+ version = "8.7"
requires = "coq.tactics"
directory = "vernac"
@@ -212,7 +216,7 @@ package "vernac" (
package "stm" (
description = "Coq State Transactional Machine"
- version = "8.6"
+ version = "8.7"
requires = "coq.vernac"
directory = "stm"
@@ -225,7 +229,7 @@ package "stm" (
package "toplevel" (
description = "Coq Toplevel"
- version = "8.6"
+ version = "8.7"
requires = "coq.stm"
directory = "toplevel"
@@ -238,7 +242,7 @@ package "toplevel" (
package "highparsing" (
description = "Coq Extra Parsing"
- version = "8.6"
+ version = "8.7"
requires = "coq.toplevel"
directory = "parsing"
@@ -251,12 +255,12 @@ package "highparsing" (
package "ltac" (
description = "Coq LTAC Plugin"
- version = "8.6"
+ version = "8.7"
requires = "coq.highparsing"
- directory = "ltac"
+ directory = "plugins/ltac"
- archive(byte) = "ltac.cma"
- archive(native) = "ltac.cmxa"
+ archive(byte) = "ltac_plugin.cmo"
+ archive(native) = "ltac_plugin.cmx"
)
diff --git a/Makefile.install b/Makefile.install
index 4800ea0b96..bde0355519 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -104,11 +104,12 @@ install-library:
$(MKDIR) $(FULLCOQLIB)
$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
$(MKDIR) $(FULLCOQLIB)/user-contrib
+ $(MKDIR) $(FULLCOQLIB)/kernel/byterun
ifndef CUSTOM
- $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
+ $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)/kernel/byterun
endif
ifeq ($(BEST),opt)
- $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
+ $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)/kernel/byterun
$(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT)
endif
# csdpcert is not meant to be directly called by the user; we install
diff --git a/configure.ml b/configure.ml
index e711367510..82ce931d67 100644
--- a/configure.ml
+++ b/configure.ml
@@ -926,7 +926,7 @@ let config_runtime () =
| _ ->
let ld="CAML_LD_LIBRARY_PATH" in
build_loadpath := sprintf "export %s:='%s/kernel/byterun':$(%s)" ld coqtop ld;
- ["-dllib";"-lcoqrun";"-dllpath";libdir]
+ ["-dllib";"-lcoqrun";"-dllpath";libdir/"kernel/byterun"]
let vmbyteflags = config_runtime ()
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 78ae7f02f9..fbcf9be1d6 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -1,8 +1,11 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-svn checkout https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color color
+Color_CI_SVNURL=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color
+Color_CI_DIR=${CI_BUILD_DIR}/color
-( cd color && make -j ${NJOBS} )
+svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR}
+
+( cd ${Color_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 412da626fd..6f624ab6ec 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
set -xe
@@ -8,20 +8,30 @@ export PATH=`pwd`/bin:$PATH
ls `pwd`/bin
+# Where we clone and build external developments
+CI_BUILD_DIR=`pwd`/_build_ci
+
# Maybe we should just use Ruby...
mathcomp_CI_BRANCH=master
mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git
+mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
-# git_checkout branch
+# git_checkout branch url dest will create a git repository
+# in <dest> (if it does not exist already) and checkout the
+# remote branch <branch> from <url>
git_checkout()
{
local _BRANCH=${1}
local _URL=${2}
local _DEST=${3}
- echo "Checking out ${_DEST}"
- git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST}
- ( cd ${3} && echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
+ mkdir -p ${_DEST}
+ ( cd ${_DEST} && \
+ if [ ! -d .git ] ; then git clone --depth 1 ${_URL} . ; fi && \
+ echo "Checking out ${_DEST}" && \
+ git fetch ${_URL} ${_BRANCH} && \
+ git checkout FETCH_HEAD && \
+ echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
}
checkout_mathcomp()
@@ -34,8 +44,8 @@ install_ssreflect()
{
echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
- checkout_mathcomp math-comp
- ( cd math-comp/mathcomp && \
+ checkout_mathcomp ${mathcomp_CI_DIR}
+ ( cd ${mathcomp_CI_DIR}/mathcomp && \
sed -i.bak '/ssrtest/d' Make && \
sed -i.bak '/odd_order/d' Make && \
sed -i.bak '/all\/all.v/d' Make && \
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index ec09389f8e..111222ac7f 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -1,13 +1,14 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
CompCert_CI_BRANCH=master
CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git
+CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert
opam install -j ${NJOBS} -y menhir
-git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert
+git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
# Patch to avoid the upper version limit
-( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
+( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 94bd5e468f..9dfdb87451 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -1,12 +1,14 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
+Coquelicot_CI_BRANCH=master
+Coquelicot_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git
+Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot
+
install_ssreflect
-# Setup coquelicot
-git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot
+git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR}
-( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
+( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
index 18d7561804..0e791ebbfd 100755
--- a/dev/ci/ci-cpdt.sh
+++ b/dev/ci/ci-cpdt.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index c669195ddd..7fc0dae2c0 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -1,9 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-git_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto
+fiat_crypto_CI_BRANCH=master
+fiat_crypto_CI_GITURL=https://github.com/mit-plv/fiat-crypto.git
+fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto
-( cd fiat-crypto && make -j ${NJOBS} )
+git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR}
+
+( cd ${fiat_crypto_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index 15d73078fd..0b3312e878 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -1,12 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
fiat_parsers_CI_BRANCH=master
fiat_parsers_CI_GITURL=https://github.com/mit-plv/fiat.git
+fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
-git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} fiat
+git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
-( cd fiat && make -j ${NJOBS} parsers )
+( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index 345924e40a..30eca7a3e9 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -1,9 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-git_checkout master https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git flocq
+Flocq_CI_BRANCH=master
+Flocq_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git
+Flocq_CI_DIR=${CI_BUILD_DIR}/flocq
-( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
+git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR}
+
+( cd ${Flocq_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 29667b018a..7b5950c887 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -1,15 +1,15 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-# XXX: replace by generic template
GeoCoq_CI_BRANCH=master
GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git
+GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq
-git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq
+git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR}
-( cd GeoCoq && \
+( cd ${GeoCoq_CI_DIR} && \
./configure.sh && \
sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \
sed -i.bak '/Elements\/Book_1\.v/d' Make && \
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 0c07564c02..62733c9452 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -1,8 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT
+HoTT_CI_BRANCH=mz-8.7
+HoTT_CI_GITURL=https://github.com/ejgallego/HoTT.git
+HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT
-( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} )
+git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR}
+
+( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} )
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index c21af976f4..10f2c2b4bd 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -1,17 +1,26 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
+stdpp_CI_BRANCH=master
+stdpp_CI_GITURL=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git
+stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp
+
+Iris_CI_BRANCH=master
+Iris_CI_GITURL=https://gitlab.mpi-sws.org/FP/iris-coq.git
+Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq
+
install_ssreflect
# Setup stdpp
-git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp
-( cd coq-stdpp && make -j ${NJOBS} && make install )
+git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR}
+
+( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install )
# Setup Iris
-git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq
-( cd iris-coq && make -j ${NJOBS} )
+git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR}
+
+( cd ${Iris_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 4450dc0710..e6a57404fe 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -1,12 +1,24 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-git_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes
-( cd math-classes && make -j ${NJOBS} && make install )
+math_classes_CI_BRANCH=v8.6
+math_classes_CI_GITURL=https://github.com/math-classes/math-classes.git
+math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
-git_checkout v8.6 https://github.com/c-corn/corn.git corn
-( cd corn && make -j ${NJOBS} )
+Corn_CI_BRANCH=v8.6
+Corn_CI_GITURL=https://github.com/c-corn/corn.git
+Corn_CI_DIR=${CI_BUILD_DIR}/corn
+# Setup Math-Classes
+
+git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
+
+( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install )
+
+# Setup Corn
+
+git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
+
+( cd ${Corn_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index 2eb150cb52..bb8188da4e 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -1,13 +1,15 @@
-#!/bin/bash
+#!/usr/bin/env bash
# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-checkout_mathcomp math-comp
+mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
+
+checkout_mathcomp ${mathcomp_CI_DIR}
# odd_order takes too much time for travis.
-( cd math-comp/mathcomp && \
+( cd ${mathcomp_CI_DIR}/mathcomp && \
sed -i.bak '/PFsection/d' Make && \
sed -i.bak '/stripped_odd_order_theorem/d' Make && \
make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index 91a33695b0..1ea56af29a 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -1,16 +1,24 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-# MetaCoq + UniCoq
+unicoq_CI_BRANCH=master
+unicoq_CI_GITURL=https://github.com/unicoq/unicoq.git
+unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
-git_checkout master https://github.com/unicoq/unicoq.git unicoq
+metacoq_CI_BRANCH=master
+metacoq_CI_GITURL=https://github.com/MetaCoq/MetaCoq.git
+metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
-( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+# Setup UniCoq
-git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq
+git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR}
-( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
+( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+# Setup MetaCoq
+
+git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR}
+
+( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 5e41211f1a..c451bf26a1 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh
new file mode 100755
index 0000000000..700105aed4
--- /dev/null
+++ b/dev/ci/ci-template.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Template_CI_BRANCH=master
+Template_CI_GITURL=https://github.com/Template/Template
+Template_CI_DIR=${CI_BUILD_DIR}/Template
+
+git_checkout ${Template_CI_BRANCH} ${Template_CI_GITURL} ${Template_CI_DIR}
+
+( cd ${Template_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
index b946324924..415f9b38f9 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -1,8 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc
+tlc_CI_BRANCH=master
+tlc_CI_GITURL=https://gforge.inria.fr/git/tlc/tlc.git
+tlc_CI_DIR=${CI_BUILD_DIR}/tlc
-( cd tlc && make -j ${NJOBS} )
+git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR}
+
+( cd ${tlc_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 15e619acbb..4c4b4f1ce1 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -1,14 +1,15 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
UniMath_CI_BRANCH=master
UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git
+UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath
-git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} UniMath
+git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR}
-( cd UniMath && \
+( cd ${UniMath_CI_DIR} && \
sed -i.bak '/Folds/d' Makefile && \
sed -i.bak '/HomologicalAlgebra/d' Makefile && \
make -j ${NJOBS} BUILD_COQ=no )
diff --git a/dev/core.dbg b/dev/core.dbg
index 698db63d23..f04e5c07b7 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -16,4 +16,4 @@ load_printer vernac.cma
load_printer stm.cma
load_printer toplevel.cma
load_printer highparsing.cma
-load_printer ltac.cma
+load_printer ltac_plugin.cmo
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 80bea0c3b1..b06ea43bdd 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -143,12 +143,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
in
(p,status)
with
- | Proof_global.NoCurrentProof -> CErrors.error "No focused proof"
- | CList.IndexOutOfRange ->
- match gi with
- | Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
- CErrors.user_err msg
- | _ -> assert false
+ Proof_global.NoCurrentProof -> CErrors.error "No focused proof"
let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 10:04:05 +0000