diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-iris-lambda-rust.sh | 6 | ||||
| -rw-r--r-- | dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh | 15 | ||||
| -rw-r--r-- | dev/dune | 1 | ||||
| -rwxr-xr-x | dev/dune-dbg.in | 3 | ||||
| -rw-r--r-- | dev/header.c | 2 | ||||
| -rw-r--r-- | dev/header.ml | 2 | ||||
| -rw-r--r-- | dev/header.py | 2 | ||||
| -rwxr-xr-x | dev/tools/change-header | 21 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | dev/top_printers.mli | 2 |
10 files changed, 36 insertions, 20 deletions
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index 95f143bb95..d99e140bce 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -8,14 +8,14 @@ install_ssreflect # Setup lambdaRust first git_download lambdaRust -# Extract required version of Iris -Iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +# Extract required version of Iris (avoiding "+" which does not work on MacOS :( *) +Iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup Iris git_download Iris # Extract required version of std++ -stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup std++ git_download stdpp diff --git a/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh b/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh new file mode 100644 index 0000000000..735b2ebbc3 --- /dev/null +++ b/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "10362" ] || [ "$CI_BRANCH" = "delay-poly-opaque" ]; then + + paramcoq_CI_REF=delay-poly-opaque + paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq + + elpi_CI_REF=delay-poly-opaque + elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + + coqhammer_CI_REF=delay-poly-opaque + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + + coq_dpdgraph_CI_REF=delay-poly-opaque + coq_dpdgraph_CI_GITURL=https://github.com/ppedrot/coq-dpdgraph + +fi @@ -12,6 +12,7 @@ (deps dune-dbg.in ../checker/coqchk.bc ../topbin/coqc_bin.bc + ../ide/coqide_main.bc ; This is not enough as the call to `ocamlfind` will fail :/ top_printers.cma) (action (copy dune-dbg.in dune-dbg))) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index bd0a837938..1382f4d1b6 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -6,6 +6,9 @@ case $1 in shift exe=_build/default/checker/coqchk.bc ;; + coqide) + exe=_build/default/ide/coqide_main.bc + ;; *) exe=_build/default/topbin/coqc_bin.bc ;; diff --git a/dev/header.c b/dev/header.c index 663c43b3d6..6201cb3b73 100644 --- a/dev/header.c +++ b/dev/header.c @@ -1,6 +1,6 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ /* <O___,, * (see CREDITS file for the list of authors) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ diff --git a/dev/header.ml b/dev/header.ml index 7c3ee60040..87553dcb56 100644 --- a/dev/header.ml +++ b/dev/header.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/dev/header.py b/dev/header.py index f81c8aa6a2..86114503d4 100644 --- a/dev/header.py +++ b/dev/header.py @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/dev/tools/change-header b/dev/tools/change-header index 687c02f4f1..59c6f43958 100755 --- a/dev/tools/change-header +++ b/dev/tools/change-header @@ -13,22 +13,19 @@ newheader=$2 if [ ! -f $oldheader ]; then echo Cannot read file $oldheader; exit 1; fi if [ ! -f $newheader ]; then echo Cannot read file $newheader; exit 1; fi -n=`wc -l $oldheader | sed -e "s/ *\([0-9]*\).*/\1/g"` -nsucc=`expr $n + 1` - -linea='(* -*- coding:utf-8 -*- *)' -lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)' +n=$(wc -l $oldheader | sed -e "s/ *\([0-9]*\).*/\1/g") +nsucc=$(expr $n + 1) modified=0 kept=0 -for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do - headline=`head -n 1 $i` - if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then - # Has emacs header +for i in $(git grep --name-only --fixed-strings "$(head -1 $oldheader)"); do + headline=$(head -n 1 $i) + if $(echo $headline | grep "(\* -\*- .* \*)" > /dev/null) || $(echo $headline | grep "^#\!" > /dev/null); then + # Has header head -n +$nsucc $i | tail -n $n > $i.head.tmp$$ hasheadline=1 - nnext=`expr $nsucc + 1` + nnext=$(expr $nsucc + 1) else head -n +$n $i > $i.head.tmp$$ hasheadline=0 @@ -44,9 +41,9 @@ for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o cat $newheader >> $i.tmp$$ tail -n +$nnext $i >> $i.tmp$$ mv $i.tmp$$ $i - modified=`expr $modified + 1` + modified=$(expr $modified + 1) else - kept=`expr $kept + 1` + kept=$(expr $kept + 1) fi rm $i.head.tmp$$ done diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 87b4d31054..8343853af5 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 2aa1808322..5a2144f996 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) |