From 6eefbf216bd4d674f84a7827ecb205c6e12c33d3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 26 Aug 2016 15:15:44 +0200 Subject: A proposal for recommended uniformity of style in programming Coq. Starting listing some recommendations in using the API. --- dev/doc/api.txt | 10 +++ dev/doc/style.txt | 215 +++++++++++++++++++++++++++++++++++------------------- 2 files changed, 151 insertions(+), 74 deletions(-) create mode 100644 dev/doc/api.txt (limited to 'dev') diff --git a/dev/doc/api.txt b/dev/doc/api.txt new file mode 100644 index 0000000000..5827257b53 --- /dev/null +++ b/dev/doc/api.txt @@ -0,0 +1,10 @@ +Recommendations in using the API: + +The type of terms: constr (see kernel/constr.ml and kernel/term.ml) + +- On type constr, the canonical equality on CIC (up to + alpha-conversion and cast removal) is Constr.equal +- The type constr is abstract, use mkRel, mkSort, etc. to build + elements in constr; use "kind_of_term" to analyze the head of a + constr; use destRel, destSort, etc. when the head constructor is + known diff --git a/dev/doc/style.txt b/dev/doc/style.txt index 27695a09b1..2ee3dadd77 100644 --- a/dev/doc/style.txt +++ b/dev/doc/style.txt @@ -1,75 +1,142 @@ - -<< L'uniformité du style est plus importante que le style lui-même. >> -(Kernigan & Pike, The Practice of Programming) - -Mode Emacs -========== - Tuareg, que l'on trouve ici : http://www.prism.uvsq.fr/~acohen/tuareg/ - - avec le réglage suivant : (setq tuareg-in-indent 2) - -Types récursifs et filtrages -============================ - Une barre de séparation y compris sur le premier constructeur - -type t = - | A - | B of machin - -match expr with - | A -> ... - | B x -> ... - -Remarque : à partir de la 8.2 environ, la tendance est à utiliser le -format suivant qui permet de limiter l'escalade d'indentation tout en -produisant un aspect visuel intéressant de bloc : - -type t = -| A -| B of machin - -match expr with -| A -> ... -| B x -> ... - -let f expr = match expr with -| A -> ... -| B x -> ... - -let f expr = function -| A -> ... -| B x -> ... - -Le deuxième cas est obtenu sous tuareg avec les réglages - - (setq tuareg-with-indent 0) - (setq tuareg-function-indent 0) - (setq tuareg-let-always-indent nil) /// notons que cette dernière est bien - /// pour les let mais pas pour les let-in - -Conditionnelles -=============== - if condition then - premier-cas - else - deuxieme-cas - - Si effets de bord dans les branches, utilisez begin ... end et non des - parenthèses i.e. - - if condition then begin - instr1; - instr2 - end else begin - instr3; - instr4 - end - - Si la première branche lève une exception, évitez le else i.e. - - if condition then if condition then error "machin"; - error "machin" -----> suite +<< Style uniformity is more important than style itself >> + (Kernigan & Pike, The Practice of Programming) + +OCaml Style: +- Spacing and indentation + - indent your code (using tuareg default) + - no strong constraints in formatting "let in"; possible styles are: + "let x = ... in" + "let x = + ... in" + "let + x = ... + in" + - but: no extra indentation before a "in" coming on next line, + otherwise, it first shifts further and further on the right, + reducing the amount of space available; second, it is not robust to + insertion of a new "let" + - it is established usage to have space around "|" as in + "match c with + | [] | [a] -> ... + | a::b::l -> ..." + - in a one-line "match", it is preferred to have no "|" in front of + the first case (this saves spaces for the match to hold in the line) + - from about 8.2, the tendency is to use the following format which + limit excessive indentation while providing an interesting "block" aspect + type t = + | A + | B of machin + + let f expr = match expr with + | A -> ... + | B x -> ... + + let f expr = function + | A -> ... + | B x -> ... + - add spaces around = and == (make the code "breaths") + - the common usage is to write "let x,y = ... in ..." rather than + "let (x,y) = ... in ..." + - parenthesizing with either "(" and ")" or with "begin" and "end" is + common practice + - preferred layout for conditionals: + if condition then + premier-cas else - suite - - + deuxieme-cas + - in case of effects in branches, use "begin ... end" rather than + parentheses + if condition then begin + instr1; + instr2 + end else begin + instr3; + instr4 + end + - if the first branch raises an exception, avoid the "else", i.e.: + if condition then if condition then error "foo"; + error "foo" -----> bar + else + bar + - it is the usage not to use ;; to end OCaml sentences (however, + inserting ";;" can be useful for debugging syntax errors crossing + the boundary of functions) + - relevant options in tuareg: + (setq tuareg-in-indent 2) + (setq tuareg-with-indent 0) + (setq tuareg-function-indent 0) + (setq tuareg-let-always-indent nil) + +- Coding methodology + - no "try ... with _ -> ..." which catches even Sys.Break (Ctrl-C), + Out_of_memory, Stack_overflow, etc. + at least, use "try with e when Errors.noncritical e -> ..." + (to be detailed, Pierre L. ?) + - do not abuse of fancy combinators: sometimes what a "let rec" loop + does is more readable and simpler to grasp than what a "fold" does + - do not break abstractions: if an internal property is hidden + behind an interface, do no rely on it in code which uses this + interface (e.g. do not use List.map thinking it is left-to-right, + use map_left) + - in particular, do not use "=" on abstract types: there is no + reason a priori that it is the intended equality on this type; use the + "equal" function normally provided with the abstract type + - avoid polymorphically typed "=" whose implementation is not + optimized in OCaml and which has moreover no reason to be the + intended implementation of the equality when it comes to be + instantiated on a particular type (e.g. use List.mem_f, + List.assoc_f, rather than List.mem, List.assoc, etc, unless it is + absolutely clear that "=" will implement the intended equality, and + with the right complexity) + - any new general-purpose enough combinator on list should be put in + cList.ml, on type option in cOpt.ml, etc. + - unless of a good reason not to so, follow the style of the + surrounding code in the same file as much as possible, + the general guidelines are otherwise "let spacing breaths" (we + have large screen nowadays), "make your code easy to read and + to understand" + - document what is tricky, but do not overdocument, sometimes the + choice of names and the structuration of the code is a better + documentation than a long discourse; use of unicode in comments is + welcome if it can make comments more readable (then + "toggle-enable-multibyte-characters" can help when using the + debugger in emacs) + - all of initial "open File", or of small-scope File.(...), or + per-ident File.foo are common practices + +- Choice of variable names + - be consistent when naming from one function to another + - be consistent with the naming adopted in the functions from the + same file, or with the naming used elsewhere by similar functions + - use variable names which express meaning + - keep "cst" for constants and avoid it for constructors which is + otherwise a source of confusion + - for constructors, use "cstr" in type constructor (resp. "cstru" in + constructor puniverse); avoid "constr" for "constructor" which + could be think as the name of an arbitrary Constr.t + - for inductive types, use "ind" in the type inductive (resp "indu" + in inductive puniverse) + - for env, use "env" + - for evar_map, use "sigma", with tolerance into "evm" and "evd" + - for named_context or rel_context, use "ctxt" or "ctx" (or "sign") + - for formal/actual indices of inductive types: "realdecls", "realargs" + - for formal/actual parameters of inductive types: "paramdecls", "paramargs" + - for terms, use e.g. c, b, a, ... + - if a term is known to be a function: f, ... + - if a term is known to be a type: t, u, typ, ... + - for a declaration, use d or "decl" + - for errors, exceptions, use e + +- Common OCaml pitfalls + - in "match ... with Case1 -> try ... with ... -> ... | Case2 -> ...", or in + "match ... with Case1 -> match ... with SubCase -> ... | Case2 -> ...", or in + parentheses are needed around the "try" and the inner "match" + - even if stream are lazy, the Pp.(++) combinator is strict and + forces the evaluation of its arguments (use a "lazy" or a "fun () ->") + to make it lazy explicitly + - in "if ... then ... else ... ++ ...", the default parenthesizing + is somehow counter-intuitive; use "(if ... then ... else ...) ++ ..." + - in "let myspecialfun = mygenericfun args", be sure that it does no + do side-effect; prefer otherwise "let mygenericfun arg = + mygenericfun args arg" to ensure that the function is evaluated at + runtime -- cgit v1.2.3 From 30a2def37ecdeeed24325089a0b0ca264100389c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 7 Feb 2017 19:37:15 +0100 Subject: [travis] [External CI] Factor out math-comp installs. We make math-comp overlays easier, we also start structuring the scripts a bit more. --- dev/ci/ci-common.sh | 43 +++++++++++++++++++++++++++++++++++++++++++ dev/ci/ci-compcert.sh | 2 +- dev/ci/ci-coquelicot.sh | 21 ++------------------- dev/ci/ci-fiat-crypto.sh | 5 +---- dev/ci/ci-flocq.sh | 2 +- dev/ci/ci-geocoq.sh | 2 +- dev/ci/ci-hott.sh | 2 +- dev/ci/ci-iris-coq.sh | 24 +++--------------------- dev/ci/ci-math-classes.sh | 4 ++-- dev/ci/ci-math-comp.sh | 10 +++++----- dev/ci/ci-metacoq.sh | 4 ++-- dev/ci/ci-tlc.sh | 2 +- 12 files changed, 63 insertions(+), 58 deletions(-) (limited to 'dev') diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 2a6601e045..087572e47d 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -4,3 +4,46 @@ set -xe export PATH=`pwd`/bin:$PATH ls `pwd`/bin + +# Maybe we should just use Ruby... +mathcomp_CI_BRANCH=master +mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git + +# git_checkout branch +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'`" ) +} + +checkout_mathcomp() +{ + git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1} +} + +# this installs just the ssreflect library of math-comp +install_ssreflect() +{ + echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' + + checkout_mathcomp math-comp + ( cd math-comp/mathcomp && \ + sed -i.bak '/ssrtest/d' Make && \ + sed -i.bak '/odd_order/d' Make && \ + sed -i.bak '/all\/all.v/d' Make && \ + sed -i.bak '/character/d' Make && \ + sed -i.bak '/real_closed/d' Make && \ + sed -i.bak '/solvable/d' Make && \ + sed -i.bak '/field/d' Make && \ + sed -i.bak '/fingroup/d' Make && \ + sed -i.bak '/algebra/d' Make && \ + make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install ) + + echo -en 'travis_fold:end:ssr.install\\r' + +} diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index d4023c9165..d4d503278a 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -4,7 +4,7 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh opam install -j ${NJOBS} -y menhir -git clone --depth 3 -b coq-8.6 https://github.com/maximedenes/CompCert.git +git_checkout coq-8.6 https://github.com/maximedenes/CompCert.git CompCert # 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} ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 4a23e51be6..94bd5e468f 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -4,26 +4,9 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://github.com/math-comp/math-comp.git - -# coquelicot just needs mathcomp -( cd math-comp/mathcomp && \ - sed -i.bak '/ssrtest/d' Make && \ - sed -i.bak '/odd_order/d' Make && \ - sed -i.bak '/all\/all.v/d' Make && \ - sed -i.bak '/character/d' Make && \ - sed -i.bak '/real_closed/d' Make && \ - sed -i.bak '/solvable/d' Make && \ - sed -i.bak '/field/d' Make && \ - sed -i.bak '/fingroup/d' Make && \ - sed -i.bak '/algebra/d' Make && \ - make -j ${NJOBS} && make install ) - -# Setup ssr -# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc -# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc +install_ssreflect # Setup coquelicot -git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git +git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot ( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index c594f83603..c669195ddd 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -4,9 +4,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://github.com/mit-plv/fiat-crypto.git +git_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto ( cd fiat-crypto && make -j ${NJOBS} ) - -# ( cd corn && make -j ${NJOBS} ) - diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index b9cf649a1a..345924e40a 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -4,6 +4,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git +git_checkout master https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git flocq ( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 589a826e02..ce870e52b5 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -7,7 +7,7 @@ source ${ci_dir}/ci-common.sh GeoCoq_CI_BRANCH=master GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git -git clone --depth 1 -b ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} +git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq ( cd GeoCoq && \ ./configure.sh && \ diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 8f82ba9f21..aaffc9d484 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 -b mz-8.6 https://github.com/ejgallego/HoTT.git +git_checkout mz-8.6 https://github.com/ejgallego/HoTT.git HoTT ( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} ) diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index e97e2c19e3..c21af976f4 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -4,32 +4,14 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# XXX: Refactor into install-ssreflect -git clone --depth 1 https://github.com/math-comp/math-comp.git - -# coquelicot just needs mathcomp -( cd math-comp/mathcomp && \ - sed -i.bak '/ssrtest/d' Make && \ - sed -i.bak '/odd_order/d' Make && \ - sed -i.bak '/all\/all.v/d' Make && \ - sed -i.bak '/character/d' Make && \ - sed -i.bak '/real_closed/d' Make && \ - sed -i.bak '/solvable/d' Make && \ - sed -i.bak '/field/d' Make && \ - sed -i.bak '/fingroup/d' Make && \ - sed -i.bak '/algebra/d' Make && \ - make -j ${NJOBS} && make install ) - -# Setup ssr = This doesn't work as coq_makefile will pass -q to coqc :S :S -# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc -# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc +install_ssreflect # Setup stdpp -git clone --depth 1 https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git +git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp ( cd coq-stdpp && make -j ${NJOBS} && make install ) # Setup Iris -git clone --depth 1 https://gitlab.mpi-sws.org/FP/iris-coq.git +git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq ( cd iris-coq && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 9127c18951..4450dc0710 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -4,9 +4,9 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 1 -b v8.6 https://github.com/math-classes/math-classes.git +git_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes ( cd math-classes && make -j ${NJOBS} && make install ) -git clone --depth 1 -b v8.6 https://github.com/c-corn/corn.git +git_checkout v8.6 https://github.com/c-corn/corn.git corn ( cd corn && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index b833792419..2eb150cb52 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -4,10 +4,10 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://github.com/math-comp/math-comp.git +checkout_mathcomp math-comp # odd_order takes too much time for travis. -( cd math-comp/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 ) +( cd math-comp/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 9a9bd3648b..91a33695b0 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -6,11 +6,11 @@ source ${ci_dir}/ci-common.sh # MetaCoq + UniCoq -git clone --depth 1 https://github.com/unicoq/unicoq.git +git_checkout master https://github.com/unicoq/unicoq.git unicoq ( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) -git clone --depth 1 https://github.com/MetaCoq/MetaCoq.git +git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq ( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index 2161a11461..b946324924 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone https://gforge.inria.fr/git/tlc/tlc.git +git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc ( cd tlc && make -j ${NJOBS} ) -- cgit v1.2.3 From 575bbed527977aee520a3954a196f5b59ae947c5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 11 Feb 2017 02:06:01 +0100 Subject: [travis] [External CI] CompCert official 8.6 support + UniMath --- dev/ci/ci-common.sh | 3 +++ dev/ci/ci-compcert.sh | 5 ++++- dev/ci/ci-unimath.sh | 15 +++++++++++++++ 3 files changed, 22 insertions(+), 1 deletion(-) create mode 100755 dev/ci/ci-unimath.sh (limited to 'dev') diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 087572e47d..412da626fd 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -2,7 +2,10 @@ set -xe +# Coq's tools need an ending slash :S, we should fix them. +export COQBIN=`pwd`/bin/ export PATH=`pwd`/bin:$PATH + ls `pwd`/bin # Maybe we should just use Ruby... diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index d4d503278a..ec09389f8e 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -3,8 +3,11 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh +CompCert_CI_BRANCH=master +CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git + opam install -j ${NJOBS} -y menhir -git_checkout coq-8.6 https://github.com/maximedenes/CompCert.git CompCert +git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert # 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} ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh new file mode 100755 index 0000000000..15e619acbb --- /dev/null +++ b/dev/ci/ci-unimath.sh @@ -0,0 +1,15 @@ +#!/bin/bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +UniMath_CI_BRANCH=master +UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git + +git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} UniMath + +( cd UniMath && \ + sed -i.bak '/Folds/d' Makefile && \ + sed -i.bak '/HomologicalAlgebra/d' Makefile && \ + make -j ${NJOBS} BUILD_COQ=no ) + -- cgit v1.2.3 From e6127d1f65a761a27c80b81c0f1bc5fca2b74af8 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Thu, 16 Feb 2017 10:24:15 -0500 Subject: [cleanup] Change Id.t option to Name.t in TacFun --- dev/doc/changes.txt | 3 +++ 1 file changed, 3 insertions(+) (limited to 'dev') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index f54f3fcc8e..2a083b360f 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -40,6 +40,9 @@ important things: - Some printing functions were moved from Pptactic to Pputils - A part of Tacexpr has been moved to Tactypes +The TacFun tactic expression constructor now takes a `Name.t list` for the +variable list rather than an `Id.t option list`. + ** Error handling ** - All error functions now take an optional parameter `?loc:Loc.t`. For -- cgit v1.2.3 From 653de32139ecee3114779a5ee2961c58793889e5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 6 Oct 2016 16:59:27 +0200 Subject: Ltac as a plugin. This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin. --- dev/ocamldebug-coq.run | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 46caca8d6f..23ad1fc017 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -32,6 +32,6 @@ exec $OCAMLDEBUG \ -I $COQTOP/plugins/ring -I $COQTOP/plugins/romega \ -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ - -I $COQTOP/plugins/xml \ + -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \ -I $COQTOP/ide \ "$@" -- cgit v1.2.3 From 6d49de4f2d1ed25b9a745378531a3b55bb0d8197 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 6 Oct 2016 18:39:28 +0200 Subject: Documenting the pluginification of Ltac. --- dev/doc/changes.txt | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'dev') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index f54f3fcc8e..8d2d055908 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -40,6 +40,24 @@ important things: - Some printing functions were moved from Pptactic to Pputils - A part of Tacexpr has been moved to Tactypes +The folder itself has been turned into a plugin. This does not change much, +but because it is a packed plugin, it may wreak havoc for third-party plugins +depending on any module defined in the ltac/ directory. Namely, even if +everything looks OK at compile time, a plugin can fail to load at link time +because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with +an error of the form: + +Error: while loading myplugin.cmxs, no implementation available for Foo. + +In particular, most EXTEND macros will trigger this problem even if they +seemingly do not use any Ltac module, as their expansion do. + +The solution is simple, and consists in adding a statement "open Ltac_plugin" +in each file using a Ltac module, before such a module is actually called. An +alternative solution would be to fully qualify Ltac modules, e.g. turning any +call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not +work for EXTEND macros though. + ** Error handling ** - All error functions now take an optional parameter `?loc:Loc.t`. For -- cgit v1.2.3 From 5efa4a5de54b681981c361fc679343790597a5d5 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 17 Feb 2017 14:25:03 +0100 Subject: remove obsolete file dev/Makefile.oug --- dev/Makefile.oug | 74 -------------------------------------------------------- 1 file changed, 74 deletions(-) delete mode 100644 dev/Makefile.oug (limited to 'dev') diff --git a/dev/Makefile.oug b/dev/Makefile.oug deleted file mode 100644 index ee69ea80df..0000000000 --- a/dev/Makefile.oug +++ /dev/null @@ -1,74 +0,0 @@ -####################################################################### -# v # The Coq Proof Assistant / The Coq Development Team # -# " --useless-elements $@ - -core_intf.oug: - $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(COREML) $(COREMLI) - -core_intf.useless: core_intf.oug - $(OUG) --load-data $< --no-reduce --print-loc --roots "" --useless-elements $@ - -# Analysis of coqchk, considering only files in the checker/ subdir - -CHECKERML:=$(call local_ml_of_cma,checker/check.cma) -CHECKERMLI:=$(call mli_of_ml,$(CHECKERML)) - -## BUG: in oug, include dirs have reversed priority compared with ocaml, cannot use CHKLIBS -MYCHKINCL:=$(MLINCLUDES) -I checker - -checker.oug: - $(OUG) --dump-data $@ -rectypes $(MYCHKINCL) $(CHECKERML) #$(CHECKERMLI) - -checker.useless: checker.oug - $(OUG) --load-data $< --no-reduce --print-loc --roots "" --useless-elements $@ - -# Analysis of extraction - -EXTRACTIONML:=$(call local_ml_of_cma,$(EXTRACTIONCMA)) -EXTRACTIONMLI:=$(call mli_of_ml,$(EXTRACTIONMLI)) - -extraction.oug: - $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(EXTRACTIONML) #$(EXTRACTIONMLI) - -extraction.useless: extraction.oug - $(OUG) --load-data $< --no-reduce --print-loc --useless-elements $@ - -# More to come ... \ No newline at end of file -- cgit v1.2.3 From 278cebe6835512a5646eafcb13e1f020c0dc5d91 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 19 Feb 2017 20:28:16 +0100 Subject: Fixing debugger after the split of toplevel into vernac. --- dev/core.dbg | 1 + dev/ocamldebug-coq.run | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/core.dbg b/dev/core.dbg index 38b9b29463..698db63d23 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -12,6 +12,7 @@ load_printer proofs.cma load_printer parsing.cma load_printer printing.cma load_printer tactics.cma +load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma load_printer highparsing.cma diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 46caca8d6f..26cfcc8ae4 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -20,7 +20,7 @@ exec $OCAMLDEBUG \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \ -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ - -I $COQTOP/pretyping -I $COQTOP/parsing \ + -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ -- cgit v1.2.3 From d9d8977cf213f0d4b2e8d324c759c23df58ba457 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 21 Feb 2017 09:46:34 +0100 Subject: [travis] track an 8.7 specific branch of HoTT. This is required since we merged PR#309: Ltac as a plugin. --- dev/ci/ci-hott.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index aaffc9d484..0c07564c02 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout mz-8.6 https://github.com/ejgallego/HoTT.git HoTT +git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT ( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} ) -- cgit v1.2.3 From 1682d4ed9df64937dfaa162e58233020036ff7b3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 23 Feb 2017 13:23:15 +0100 Subject: Fixing #use"include" after vernac is added and ltac is moved to a plugin. --- dev/base_include | 4 ++-- dev/top_printers.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'dev') diff --git a/dev/base_include b/dev/base_include index 0abcefc38e..242405ae29 100644 --- a/dev/base_include +++ b/dev/base_include @@ -17,7 +17,7 @@ #directory "grammar";; #directory "intf";; #directory "stm";; -#directory "ltac";; +#directory "vernac";; #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) @@ -195,7 +195,7 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_tac = Pcoq.parse_string Pltac.tactic;; +let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; (* build a term of type glob_constr without type-checking or resolution of diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 4fcad88202..dc354b130b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -234,7 +234,7 @@ let ppenvwithcst e = pp str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}") -let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x)) +let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) let ppobj obj = Format.print_string (Libobject.object_tag obj) -- cgit v1.2.3 From 4567e3a0a44a6c398375effa7d9a49342172512a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 24 Feb 2017 02:28:27 +0100 Subject: [travis] [External CI] fiat-parsers --- dev/ci/ci-fiat-parsers.sh | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100755 dev/ci/ci-fiat-parsers.sh (limited to 'dev') diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh new file mode 100755 index 0000000000..15d73078fd --- /dev/null +++ b/dev/ci/ci-fiat-parsers.sh @@ -0,0 +1,12 @@ +#!/bin/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 + +git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} fiat + +( cd fiat && make -j ${NJOBS} parsers ) -- cgit v1.2.3 From ae5ae4967c423a26b99666dcce441236dd7b9a7b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Mar 2017 16:33:47 +0100 Subject: [travis] Move GeoCoq to allow fail. We need to agree a bit more with upstream. --- dev/ci/ci-geocoq.sh | 2 ++ 1 file changed, 2 insertions(+) (limited to 'dev') diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index ce870e52b5..29667b018a 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -12,5 +12,7 @@ git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq ( cd GeoCoq && \ ./configure.sh && \ sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \ + sed -i.bak '/Elements\/Book_1\.v/d' Make && \ + sed -i.bak '/Elements\/Book_3\.v/d' Make && \ coq_makefile -f Make -o Makefile && \ make -j ${NJOBS} ) -- cgit v1.2.3 From 56dc3e331c6b4b2bfa5ac072db57db8250884ce3 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 7 Mar 2017 12:33:37 +0100 Subject: Improve build of travis target on local machine. - Move the git clones to a specific subfolder to avoid pollution. - Do not fail when git clone already exist (but make sure it is up-to-date). --- dev/ci/ci-common.sh | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'dev') diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 412da626fd..cc34bc2957 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -12,6 +12,9 @@ ls `pwd`/bin mathcomp_CI_BRANCH=master mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git +# Where we clone and build external developments +CI_BUILD_DIR=`pwd`/_build_ci + # git_checkout branch git_checkout() { @@ -19,9 +22,15 @@ git_checkout() 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 ${CI_BUILD_DIR} + cd ${CI_BUILD_DIR} + + if [ ! -d ${_DEST} ] ; then + echo "Checking out ${_DEST}" + git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST} + fi + ( cd ${_DEST} && git pull && + echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" ) } checkout_mathcomp() -- cgit v1.2.3 From ba36aab9ad9a3d210211e1d4527dd0f6f493ca05 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 7 Mar 2017 16:14:39 +0100 Subject: [travis] Change headband for wider compatibility. --- dev/ci/ci-color.sh | 2 +- dev/ci/ci-common.sh | 2 +- dev/ci/ci-compcert.sh | 2 +- dev/ci/ci-coquelicot.sh | 2 +- dev/ci/ci-cpdt.sh | 2 +- dev/ci/ci-fiat-crypto.sh | 2 +- dev/ci/ci-fiat-parsers.sh | 2 +- dev/ci/ci-flocq.sh | 2 +- dev/ci/ci-geocoq.sh | 2 +- dev/ci/ci-hott.sh | 2 +- dev/ci/ci-iris-coq.sh | 2 +- dev/ci/ci-math-classes.sh | 2 +- dev/ci/ci-math-comp.sh | 2 +- dev/ci/ci-metacoq.sh | 2 +- dev/ci/ci-sf.sh | 2 +- dev/ci/ci-tlc.sh | 2 +- dev/ci/ci-unimath.sh | 2 +- 17 files changed, 17 insertions(+), 17 deletions(-) (limited to 'dev') diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 78ae7f02f9..36c7b9e965 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.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-common.sh b/dev/ci/ci-common.sh index cc34bc2957..94fd00c0d2 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 diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index ec09389f8e..3b897f679a 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.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-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 94bd5e468f..2052a1e5ff 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" 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..683f9712d6 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index 15d73078fd..5e52f44116 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index 345924e40a..d398660444 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 29667b018a..7502139c2b 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.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-hott.sh b/dev/ci/ci-hott.sh index 0c07564c02..9d27be2e91 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.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-iris-coq.sh b/dev/ci/ci-iris-coq.sh index c21af976f4..7044c3859d 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 4450dc0710..c5105a8486 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 2eb150cb52..1b6c6fb847 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 91a33695b0..597a6ab7b3 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" 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-tlc.sh b/dev/ci/ci-tlc.sh index b946324924..df86b3cadd 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.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-unimath.sh b/dev/ci/ci-unimath.sh index 15e619acbb..5b7fc1c053 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -- cgit v1.2.3 From 710c1e1f49ce834acb9488704bcbbf13c4ebaf91 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 7 Mar 2017 23:30:29 +0100 Subject: [travis] Adding a template file and using it for all targets. --- dev/ci/ci-color.sh | 7 +++++-- dev/ci/ci-compcert.sh | 5 +++-- dev/ci/ci-coquelicot.sh | 10 ++++++---- dev/ci/ci-fiat-crypto.sh | 9 ++++++--- dev/ci/ci-fiat-parsers.sh | 6 +++--- dev/ci/ci-flocq.sh | 9 ++++++--- dev/ci/ci-geocoq.sh | 6 +++--- dev/ci/ci-hott.sh | 8 ++++++-- dev/ci/ci-iris-coq.sh | 19 ++++++++++++++----- dev/ci/ci-math-classes.sh | 22 +++++++++++++++++----- dev/ci/ci-math-comp.sh | 6 ++++-- dev/ci/ci-metacoq.sh | 20 ++++++++++++++------ dev/ci/ci-template.sh | 12 ++++++++++++ dev/ci/ci-tlc.sh | 8 ++++++-- dev/ci/ci-unimath.sh | 5 +++-- 15 files changed, 108 insertions(+), 44 deletions(-) create mode 100755 dev/ci/ci-template.sh (limited to 'dev') diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 36c7b9e965..fbcf9be1d6 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,6 +3,9 @@ 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-compcert.sh b/dev/ci/ci-compcert.sh index 3b897f679a..111222ac7f 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -5,9 +5,10 @@ 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 2052a1e5ff..9dfdb87451 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -1,12 +1,14 @@ #!/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-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 683f9712d6..7fc0dae2c0 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -1,9 +1,12 @@ #!/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 5e52f44116..0b3312e878 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -1,12 +1,12 @@ #!/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 d398660444..30eca7a3e9 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -1,9 +1,12 @@ #!/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 7502139c2b..7b5950c887 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -3,13 +3,13 @@ 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 9d27be2e91..62733c9452 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,6 +3,10 @@ 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 7044c3859d..10f2c2b4bd 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -1,17 +1,26 @@ #!/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 c5105a8486..e6a57404fe 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -1,12 +1,24 @@ #!/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 1b6c6fb847..bb8188da4e 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -4,10 +4,12 @@ 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 597a6ab7b3..1ea56af29a 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -1,16 +1,24 @@ #!/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-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 df86b3cadd..415f9b38f9 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -3,6 +3,10 @@ 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 5b7fc1c053..4c4b4f1ce1 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -5,10 +5,11 @@ 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 ) -- cgit v1.2.3 From fd5c5da475baea11d7ee2e1c2e965d7faeed3f33 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 8 Mar 2017 09:56:01 +0100 Subject: [travis] Make the git_checkout function more reliable. This commit also documents the behavior of said function; and fix the location of the ssreflect clone to an absolute path (this is now necessary). --- dev/ci/ci-common.sh | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) (limited to 'dev') diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 94fd00c0d2..6f624ab6ec 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -8,28 +8,29 @@ 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 -# Where we clone and build external developments -CI_BUILD_DIR=`pwd`/_build_ci - -# git_checkout branch +# git_checkout branch url dest will create a git repository +# in (if it does not exist already) and checkout the +# remote branch from git_checkout() { local _BRANCH=${1} local _URL=${2} local _DEST=${3} - mkdir -p ${CI_BUILD_DIR} - cd ${CI_BUILD_DIR} - - if [ ! -d ${_DEST} ] ; then - echo "Checking out ${_DEST}" - git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST} - fi - ( cd ${_DEST} && git pull && + 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'`" ) } @@ -43,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 && \ -- cgit v1.2.3 From e2135c2f5fd8846c30d8099eed523fe06202b614 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 12 Mar 2017 13:16:27 +0100 Subject: Updating core.dbg after ltac moved to plugins directory. --- dev/core.dbg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') 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 -- cgit v1.2.3 From 2cee6aa7a30b39c53e23fc69f0b9e7754ebee740 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 13 Mar 2017 19:53:00 +0100 Subject: [travis] Basic support for overlays. We now allow the user to overlay contribution repositories and branches by adding their own rules to `ci-basic-overlay.sh`. This just provides very basic support. --- dev/ci/ci-basic-overlay.sh | 103 +++++++++++++++++++++++++++++++++++++++++++++ dev/ci/ci-color.sh | 1 - dev/ci/ci-common.sh | 6 +-- dev/ci/ci-compcert.sh | 2 - dev/ci/ci-coquelicot.sh | 2 - dev/ci/ci-fiat-crypto.sh | 2 - dev/ci/ci-fiat-parsers.sh | 2 - dev/ci/ci-flocq.sh | 2 - dev/ci/ci-geocoq.sh | 2 - dev/ci/ci-hott.sh | 2 - dev/ci/ci-iris-coq.sh | 4 -- dev/ci/ci-math-classes.sh | 4 -- dev/ci/ci-metacoq.sh | 5 --- dev/ci/ci-sf.sh | 3 +- dev/ci/ci-tlc.sh | 2 - dev/ci/ci-unimath.sh | 2 - dev/ci/ci-user-overlay.sh | 22 ++++++++++ 17 files changed, 130 insertions(+), 36 deletions(-) create mode 100644 dev/ci/ci-basic-overlay.sh create mode 100644 dev/ci/ci-user-overlay.sh (limited to 'dev') diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh new file mode 100644 index 0000000000..da5b425794 --- /dev/null +++ b/dev/ci/ci-basic-overlay.sh @@ -0,0 +1,103 @@ +#!/usr/bin/env bash + +# This is the basic overlay set for repositories in the CI. + +# Maybe we should just use Ruby to have real objects... + +######################################################################## +# MathComp +######################################################################## +: ${mathcomp_CI_BRANCH:=master} +: ${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git} + +######################################################################## +# UniMath +######################################################################## +: ${UniMath_CI_BRANCH:=master} +: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git} + +######################################################################## +# Unicoq + Metacoq +######################################################################## +: ${unicoq_CI_BRANCH:=master} +: ${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git} + +: ${metacoq_CI_BRANCH:=master} +: ${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git} + +######################################################################## +# Mathclasses + Corn +######################################################################## +: ${math_classes_CI_BRANCH:=v8.6} +: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git} + +: ${Corn_CI_BRANCH:=v8.6} +: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git} + +######################################################################## +# Iris +######################################################################## +: ${stdpp_CI_BRANCH:=master} +: ${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git} + +: ${Iris_CI_BRANCH:=master} +: ${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git} + +######################################################################## +# HoTT +######################################################################## +: ${HoTT_CI_BRANCH:=mz-8.7} +: ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git} + +######################################################################## +# GeoCoq +######################################################################## +: ${GeoCoq_CI_BRANCH:=master} +: ${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git} + +######################################################################## +# Flocq +######################################################################## +: ${Flocq_CI_BRANCH:=master} +: ${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git} + +######################################################################## +# Coquelicot +######################################################################## +: ${Coquelicot_CI_BRANCH:=master} +: ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git} + +######################################################################## +# Coquelicot +######################################################################## +: ${CompCert_CI_BRANCH:=master} +: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} + +######################################################################## +# fiat_parsers +######################################################################## +: ${fiat_parsers_CI_BRANCH:=master} +: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git} + +######################################################################## +# fiat_crypto +######################################################################## +: ${fiat_crypto_CI_BRANCH:=master} +: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git} + +######################################################################## +# CoLoR +######################################################################## +: ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color} + +######################################################################## +# SF +######################################################################## +: ${sf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz} + +######################################################################## +# TLC +######################################################################## +: ${tlc_CI_BRANCH:=master} +: ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git} + diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index fbcf9be1d6..3f0716511d 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,7 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -Color_CI_SVNURL=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color Color_CI_DIR=${CI_BUILD_DIR}/color svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR} diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 6f624ab6ec..c94f150263 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -11,9 +11,9 @@ 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 +source ${ci_dir}/ci-user-overlay.sh +source ${ci_dir}/ci-basic-overlay.sh + mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp # git_checkout branch url dest will create a git repository diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 111222ac7f..c78ffdc2c0 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -3,8 +3,6 @@ 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 diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 9dfdb87451..40eff03b78 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -3,8 +3,6 @@ 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 diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 7fc0dae2c0..93d39aab07 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -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 git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR} diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index 0b3312e878..c62aa1d859 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -3,8 +3,6 @@ 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_parsers_CI_DIR} diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index 30eca7a3e9..ec19bd9939 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -Flocq_CI_BRANCH=master -Flocq_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git Flocq_CI_DIR=${CI_BUILD_DIR}/flocq git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR} diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 7b5950c887..4e5aa2687b 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -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_CI_DIR} diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 62733c9452..1bf6e9a872 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -HoTT_CI_BRANCH=mz-8.7 -HoTT_CI_GITURL=https://github.com/ejgallego/HoTT.git HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index 10f2c2b4bd..eb1d1be078 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -3,12 +3,8 @@ 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 diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index e6a57404fe..beb75773b7 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -3,12 +3,8 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -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 -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 diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 1ea56af29a..e31691179e 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -3,12 +3,7 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -unicoq_CI_BRANCH=master -unicoq_CI_GITURL=https://github.com/unicoq/unicoq.git unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq - -metacoq_CI_BRANCH=master -metacoq_CI_GITURL=https://github.com/MetaCoq/MetaCoq.git metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq # Setup UniCoq diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index c451bf26a1..7d23ccad97 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -3,7 +3,8 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -wget https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz +# XXX: Needs fixing to properly set the build directory. +wget ${sf_CI_TARURL} tar xvfz sf.tgz ( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index 415f9b38f9..ce26399378 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -tlc_CI_BRANCH=master -tlc_CI_GITURL=https://gforge.inria.fr/git/tlc/tlc.git tlc_CI_DIR=${CI_BUILD_DIR}/tlc git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR} diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 4c4b4f1ce1..175b82b5f9 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -3,8 +3,6 @@ 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_CI_DIR} diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh new file mode 100644 index 0000000000..0285747432 --- /dev/null +++ b/dev/ci/ci-user-overlay.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash + +# Add user overlays here. You can use some logic to detect if you are +# in your travis branch and conditionally enable the overlay. + +# Some useful Travis variables: +# (https://docs.travis-ci.com/user/environment-variables/#Default-Environment-Variables) +# +# - TRAVIS_BRANCH: For builds not triggered by a pull request this is +# the name of the branch currently being built; whereas for builds +# triggered by a pull request this is the name of the branch +# targeted by the pull request (in many cases this will be master). +# +# - TRAVIS_COMMIT: The commit that the current build is testing. +# +# - TRAVIS_PULL_REQUEST: The pull request number if the current job is +# a pull request, “false” if it’s not a pull request. +# +# - TRAVIS_PULL_REQUEST_BRANCH: If the current job is a pull request, +# the name of the branch from which the PR originated. "" if the +# current job is a push build. + -- cgit v1.2.3 From becc6ef43a0f838d1f6388e8c7373c13f26082bc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 21 Mar 2017 15:12:27 +0100 Subject: trivial: fix comment --- dev/ci/ci-basic-overlay.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index da5b425794..241ec35861 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -68,7 +68,7 @@ : ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git} ######################################################################## -# Coquelicot +# CompCert ######################################################################## : ${CompCert_CI_BRANCH:=master} : ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} -- cgit v1.2.3 From 2633ab1f433a290acbc2ec77d8ae05ec3ba64ec4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 21 Mar 2017 15:40:31 +0100 Subject: [safe-string] update dev/doc/changes --- dev/doc/changes.txt | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'dev') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 12c3ec4546..3dc6973ba0 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,12 @@ = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = ========================================= +* Ocaml * + +Coq is compiled with -safe-string enabled and requires plugins to do +the same. This means that code using `String` in an imperative way +will fail to compile now. They should switch to `Bytes.t` + * ML API * We renamed the following functions: -- cgit v1.2.3 From 5b8bfee9d80e550cd81e326ec134430b2a4797a5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Sep 2016 16:30:21 +0200 Subject: [pp] Make feedback the only logging mechanism. Previously to this patch, Coq featured to distinct logging paths: the console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format` module, and the `Feedback` one, intended to encapsulate message inside a more general, GUI-based feedback protocol. This patch removes the legacy logging path and makes feedback canonical. Thus, the core of Coq has no dependency on console code anymore. Additionally, this patch resolves the duplication of "document" formats present in the same situation. The original console-based printing code relied on an opaque datatype `std_ppcmds`, (mostly a reification of `Format`'s format strings) that could be then rendered to the console. However, the feedback path couldn't reuse this type due to its opaque nature. The first versions just embedded rending of `std_ppcmds` to a string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was introduced. The idea for this type was to be serializable, however it brought several problems: it didn't have proper document manipulation operations, its format was overly verbose and didn't preserve the full layout, and it still relied on `Format` for generation, making client-side rendering difficult. We thus follow the plan outlined in CEP#9, that is to say, we take a public and refactored version of `std_ppcmds` as the canonical "document type", and move feedback to be over there. The toplevel now is implemented as a feedback listener and has ownership of the console. `richpp` is now IDE-specific, and only used for legacy rendering. It could go away in future versions. `std_ppcmds` carries strictly more information and is friendlier to client-side rendering and display control. Thus, the new panorama is: - `Feedback` has become a very module for event dispatching. - `Pp` contains a target-independent box-based document format. It also contains the `Format`-based renderer. - All console access lives in `toplevel`, with console handlers private to coqtop. _NOTE_: After this patch, many printing parameters such as printing width or depth should be set client-side. This works better IMO, clients don't need to notify Coq about resizing anywmore. Indeed, for box-based capable backends such as HTML or LaTeX, the UI can directly render and let the engine perform the word breaking work. _NOTE_: Many messages could benefit from new features of the output format, however we have chosen not to alter them to preserve output. A Future commits will move console tag handling in `Pp_style` to `toplevel/`, where it logically belongs. The only change with regards to printing is that the "Error:" header was added to console output in several different positions, we have removed some of this duplication, now error messages should be a bit more consistent. --- dev/doc/changes.txt | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++++ dev/top_printers.ml | 2 +- 2 files changed, 53 insertions(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 12c3ec4546..53e9a282fa 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -70,6 +70,58 @@ work for EXTEND macros though. - The header parameter to `user_err` has been made optional. +** Pretty printing ** + +Some functions have been removed, see pretty printing below for more +details. + +* Pretty Printing and XML protocol * + +The type std_cmdpps has been reworked and made the canonical "Coq rich +document type". This allows for a more uniform handling of printing +(specially in IDEs). The main consequences are: + + - Richpp has been confined to IDE use. Most of previous uses of the + `richpp` type should be replaced now by `Pp.std_cmdpps`. Main API + has been updated. + + - The XML protocol will send a new message type of `pp`, which should + be rendered client-wise. + + - `Set Printing Width` is deprecated, now width is controlled + client-side. + + - `Pp_control` has removed. The new module `Topfmt` implements + console control for the toplevel. + + - The impure tag system in Pp has been removed. This also does away + with the printer signatures and functors. Now printers tag + unconditionally. + + - The following functions have been removed from `Pp`: + + val stras : int * string -> std_ppcmds + val tbrk : int * int -> std_ppcmds + val tab : unit -> std_ppcmds + val pifb : unit -> std_ppcmds + val comment : int -> std_ppcmds + val comments : ((int * int) * string) list ref + val eval_ppcmds : std_ppcmds -> std_ppcmds + val is_empty : std_ppcmds -> bool + val t : std_ppcmds -> std_ppcmds + val hb : int -> std_ppcmds + val vb : int -> std_ppcmds + val hvb : int -> std_ppcmds + val hovb : int -> std_ppcmds + val tb : unit -> std_ppcmds + val close : unit -> std_ppcmds + val tclose : unit -> std_ppcmds + val open_tag : Tag.t -> std_ppcmds + val close_tag : unit -> std_ppcmds + val msg_with : ... + + module Tag + ========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/dev/top_printers.ml b/dev/top_printers.ml index dc354b130b..cd464801b0 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -29,7 +29,7 @@ let _ = set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) (* std_ppcmds *) -let pp x = Pp.pp_with !Pp_control.std_ft x +let pp x = Pp.pp_with !Topfmt.std_ft x (** Future printer *) -- cgit v1.2.3 From 44b2c7979e1ea3a834f4e9bd2fcd631d568b895e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Mar 2017 17:17:33 +0100 Subject: [travis] Fix iris-coq build. We need to do a bit of hacking, but it should be fine for the short term. c.f. https://gitlab.mpi-sws.org/FP/iris-coq/issues/83 --- dev/ci/ci-common.sh | 8 ++++++-- dev/ci/ci-iris-coq.sh | 14 +++++++++----- 2 files changed, 15 insertions(+), 7 deletions(-) (limited to 'dev') diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index c94f150263..2711b7ecaa 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -25,12 +25,16 @@ git_checkout() local _URL=${2} local _DEST=${3} + # Allow an optional 4th argument for the commit + local _COMMIT=${4:-FETCH_HEAD} + local _DEPTH=$(if [ -z "${4}" ]; then echo "--depth 1"; fi) + mkdir -p ${_DEST} ( cd ${_DEST} && \ - if [ ! -d .git ] ; then git clone --depth 1 ${_URL} . ; fi && \ + if [ ! -d .git ] ; then git clone ${_DEPTH} ${_URL} . ; fi && \ echo "Checking out ${_DEST}" && \ git fetch ${_URL} ${_BRANCH} && \ - git checkout FETCH_HEAD && \ + git checkout ${_COMMIT} && \ echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" ) } diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index eb1d1be078..262dd6fa01 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -9,14 +9,18 @@ Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq install_ssreflect -# Setup stdpp +# Setup Iris first, as it is needed to compute the dependencies -git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} +git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR} +read -a IRIS_DEP < ${Iris_CI_DIR}/opam.pins -( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install ) +# Setup stdpp +stdpp_CI_GITURL=${IRIS_DEP[1]}.git +stdpp_CI_COMMIT=${IRIS_DEP[2]} -# Setup Iris +git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT} -git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR} +( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install ) +# Build iris now ( cd ${Iris_CI_DIR} && make -j ${NJOBS} ) -- cgit v1.2.3 From f29e577ef81e608cb8b3a68f4e171716c1280711 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 20 Mar 2017 13:38:14 +0100 Subject: [travis] Add VST --- dev/ci/ci-basic-overlay.sh | 9 +++++++++ dev/ci/ci-vst.sh | 13 +++++++++++++ 2 files changed, 22 insertions(+) create mode 100755 dev/ci/ci-vst.sh (limited to 'dev') diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 241ec35861..336ce9d8f1 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -46,8 +46,11 @@ ######################################################################## # HoTT ######################################################################## +# Temporal overlay : ${HoTT_CI_BRANCH:=mz-8.7} : ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git} +# : ${HoTT_CI_BRANCH:=master} +# : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git} ######################################################################## # GeoCoq @@ -73,6 +76,12 @@ : ${CompCert_CI_BRANCH:=master} : ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} +######################################################################## +# VST +######################################################################## +: ${VST_CI_BRANCH:=master} +: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git} + ######################################################################## # fiat_parsers ######################################################################## diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh new file mode 100755 index 0000000000..c111951852 --- /dev/null +++ b/dev/ci/ci-vst.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +VST_CI_DIR=${CI_BUILD_DIR}/VST + +# opam install -j ${NJOBS} -y menhir +git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR} + +# Targets are: msl veric floyd +# Patch to avoid the upper version limit +( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make -j ${NJOBS} ) -- cgit v1.2.3