DeepSpec / InteractionTrees

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

Adapt to alpha-renaming in coq-paco dev #253

Closed Lysxia closed 1 year ago

RyanGlScott commented 1 year ago

Would you be willing to make a new release with these changes? I ask since opam install coq-itree appears to be broken at the moment:

$ opam install coq-itree
The following actions will be performed:
  ∗ install coq-paco    4.2.0  [required by coq-itree]
  ∗ install coq-ext-lib 0.11.8 [required by coq-itree]
  ∗ install coq-itree   5.1.0
===== ∗ 3 =====
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved coq-ext-lib.0.11.8  (cached)
⬇ retrieved coq-itree.5.1.0  (cached)
⬇ retrieved coq-paco.4.2.0  (cached)
∗ installed coq-ext-lib.0.11.8
∗ installed coq-paco.4.2.0
[ERROR] The compilation of coq-itree.5.1.0 failed at "dune build -p coq-itree -j 11 @install".

#=== ERROR while compiling coq-itree.5.1.0 ====================================#
# context     2.1.2 | linux/x86_64 | ocaml-base-compiler.4.14.0 | https://coq.inria.fr/opam/released#2023-03-13 21:00
# path        ~/.opam/4.14.0-coq-8.15.2/.opam-switch/build/coq-itree.5.1.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-itree -j 11 @install
# exit-code   1
# env-file    ~/.opam/log/coq-itree-1165833-cfce3c.env
# output-file ~/.opam/log/coq-itree-1165833-cfce3c.out
### output ###
# (cd _build/default && /home/rscott/.opam/4.14.0-coq-8.15.2/bin/coqc -q -R theories ITree theories/Eq/Paco2.v)
# File "./theories/Eq/Paco2.v", line 27, characters 75-77:
# Error: The reference x1 was not found in the current environment.
#

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build coq-itree 5.1.0
└─
┌─ The following changes have been performed
│ ∗ install coq-ext-lib 0.11.8
│ ∗ install coq-paco    4.2.0
└─

The former state can be restored with:
    /usr/local/bin/opam switch import "/home/rscott/.opam/4.14.0-coq-8.15.2/.opam-switch/backup/state-20230314195753.export"
Lysxia commented 1 year ago

I can make a release some time this week. I can add an upper bound on already released versions and in the very short term you can opam pin add coq-paco 4.1.2.

RyanGlScott commented 1 year ago

Thanks! Adding upper bounds would be sufficient for my needs.