Findlib error: diaframe.diaframe-plugin not found
Hi Ike,
I hope you are doing well! Very exciting to see you soon in Neijmegen! I recently encountered a weird error after updating my coq installation:
Findlib error: diaframe.diaframe-plugin not found in:
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/ltac2
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/ssrmatching
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/tutorial
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/tutorial/p3
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/tutorial/p2
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/tutorial/p0
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/tutorial/p1
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/zify
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/number_string_notation
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/funind
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/micromega
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/rtauto
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/derive
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/ssreflect
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/cc
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/ring
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/nsatz
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/tauto
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/btauto
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/extraction
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/ltac
/Users/anton/.opam/AddressC/lib/coq/../coq-core/plugins/firstorder
/Users/anton/.opam/AddressC/lib/coq/../coq-core/..
/Users/anton/.opam/AddressC/lib/coq/user-contrib/Ltac2
/Users/anton/.opam/AddressC/lib/coq/user-contrib/iris
/Users/anton/.opam/AddressC/lib/coq/user-contrib/iris/heap_lang
/Users/anton/.opam/AddressC/lib/coq/user-contrib/iris/heap_lang/lib
/Users/anton/.opam/AddressC/lib/coq/user-contrib/iris/bi
/Users/anton/.opam/AddressC/lib/coq/user-contrib/iris/bi/lib
/Users/anton/.opam/AddressC/lib/coq/user-contrib/iris/base_logic
/Users/anton/.opam/AddressC/lib/coq/user-contrib/iris/base_logic/lib
/Users/anton/.opam/AddressC/lib/coq/user-contrib/iris/proofmode
/Users/anton/.opam/AddressC/lib/coq/user-contrib/iris/prelude
/Users/anton/.opam/AddressC/lib/coq/user-contrib/iris/program_logic
/Users/anton/.opam/AddressC/lib/coq/user-contrib/iris/si_logic
/Users/anton/.opam/AddressC/lib/coq/user-contrib/iris/algebra
/Users/anton/.opam/AddressC/lib/coq/user-contrib/iris/algebra/lib
/Users/anton/.opam/AddressC/lib/coq/user-contrib/Equations
/Users/anton/.opam/AddressC/lib/coq/user-contrib/Equations/Prop
/Users/anton/.opam/AddressC/lib/coq/user-contrib/Equations/Type
/Users/anton/.opam/AddressC/lib/coq/user-contrib/diaframe
/Users/anton/.opam/AddressC/lib/coq/user-contrib/diaframe/heap_lang
/Users/anton/.opam/AddressC/lib/coq/user-contrib/diaframe/heap_lang/examples
/Users/anton/.opam/AddressC/lib/coq/user-contrib/diaframe/heap_lang/examples/base
/Users/anton/.opam/AddressC/lib/coq/user-contrib/diaframe/hint_search
/Users/anton/.opam/AddressC/lib/coq/user-contrib/diaframe/symb_exec
/Users/anton/.opam/AddressC/lib/coq/user-contrib/diaframe/steps
/Users/anton/.opam/AddressC/lib/coq/user-contrib/diaframe/lib
/Users/anton/.opam/AddressC/lib/coq/user-contrib/diaframe/lib/own
/Users/anton/.opam/AddressC/lib/coq/user-contrib/stdpp
/Users/anton/.opam/AddressC/lib
My versions are:
coq 8.17.1 The Coq Proof Assistant
coq-core 8.17.1 The Coq Proof Assistant -- Core Binaries and Tools
coq-diaframe dev.2023-09-27.0.cdfac25b Diaframe: Automation for Iris
coq-diaframe-heap-lang dev.2023-09-27.0.cdfac25b Diaframe: Automation for Iris's Heap Lang
coq-equations 1.3+8.17 A function definition package for Coq
coq-iris dev.2023-09-21.2.d063b13b A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
coq-iris-heap-lang dev.2023-09-21.2.d063b13b The canonical example language for Iris
coq-stdlib 8.17.1 The Coq Proof Assistant -- Standard Library
coq-stdpp dev.2023-09-21.2.7f6df4fa An extended "Standard Library" for Coq
coqide-server 8.17.1 The Coq Proof Assistant, XML protocol server
This error didn't happen for:
coq 8.17.0 The Coq Proof Assistant
coq-core 8.17.0 The Coq Proof Assistant -- Core Binaries and Tools
coq-diaframe dev.2023-06-15.0.1c3b5549 Diaframe: Automation for Iris
coq-diaframe-heap-lang dev.2023-06-15.0.1c3b5549 Diaframe: Automation for Iris's Heap Lang
coq-equations 1.3+8.17 A function definition package for Coq
coq-iris dev.2023-06-14.0.f0e415b6 A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
coq-iris-heap-lang dev.2023-06-14.0.f0e415b6 The canonical example language for Iris
coq-stdlib 8.17.0 The Coq Proof Assistant -- Standard Library
coq-stdpp dev.2023-06-01.0.d1254759 An extended "Standard Library" for Coq
The code is in the AddressC repository: https://github.com/koka-lang/AddressC
(just run make
to reproduce). Do you have an idea what might have caused this?