DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
203 stars 51 forks source link

only works with paco 2.0.2 #92

Closed liyishuai closed 5 years ago

liyishuai commented 5 years ago

Paco 2.0.3 causes error:

#=== ERROR while compiling coq-itree.dev ======================================#
# context              2.0.2 | linux/x86_64 | ocaml-base-compiler.4.05.0 | https://coq.inria.fr/opam/extra-dev#2019-03-05 21:12
# path                 ~/.opam/4.05.0/.opam-switch/build/coq-itree.dev
# command              /usr/bin/make -j1
# exit-code            2
# env-file             ~/.opam/log/coq-itree-747-eec089.env
# output-file          ~/.opam/log/coq-itree-747-eec089.out
### output ###
# [...]
# COQC theories/Eq/Eq.v
# File "./theories/Eq/Eq.v", line 454, characters 16-22:
# Error: Ltac call to "pupto2" failed.
#        No applicable tactic.
# 
# Makefile.coq:656: recipe for target 'theories/Eq/Eq.vo' failed
# make[2]: *** [theories/Eq/Eq.vo] Error 1
# Makefile.coq:317: recipe for target 'all' failed
# make[1]: *** [all] Error 2
# make[1]: Leaving directory '/home/coq/.opam/4.05.0/.opam-switch/build/coq-itree.dev'
# Makefile:8: recipe for target 'coq' failed
# make: *** [coq] Error 2
Lysxia commented 5 years ago

Thanks!