diff options
Diffstat (limited to 'dev/ci')
| -rwxr-xr-x | dev/ci/ci-sf.sh | 19 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh | 4 |
2 files changed, 23 insertions, 0 deletions
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 272041205c..217540cc19 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -14,6 +14,25 @@ tar xvfz vfa.tgz sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v +# Delete useless calls to try omega; unfold +patch vfa/SearchTree.v <<EOF +*** SearchTree.v.bak 2017-09-06 19:12:59.000000000 +0200 +--- SearchTree.v 2017-11-21 16:34:41.000000000 +0100 +*************** +*** 674,683 **** + forall i j : key, ~ (i > j) -> ~ (i < j) -> i=j. + Proof. + intros. +- try omega. (* Oops! [omega] cannot solve this one. +- The problem is that [i] and [j] have type [key] instead of type [nat]. +- The solution is easy enough: *) +- unfold key in *. + omega. + + (** So, if you get stuck on an [omega] that ought to work, +--- 674,679 ---- +EOF + ( cd lf && make clean && make ) ( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make ) diff --git a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh new file mode 100644 index 0000000000..c9f1272bed --- /dev/null +++ b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6197" ] || [ "$TRAVIS_BRANCH" = "plugins+remove_locality_hack" ]; then + ltac2_CI_BRANCH=localityfixyou + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2.git +fi |