Comments (13)
Hi, thanks for the report!
Can you check proof-omit-proofs-option
(C-h v proof-omit-proofs-option)? If it is t
, please try again after setting it to nil
.
from pg.
I've only set the options listed above, everything else is at default level.
The command you described says "Its value is nil".
from pg.
OCaml plugins are not supported, see https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General/#Current-Limitations, nevertheless I wanted to investigate, but I was not able to install diaframe.
I have an opam switch with
coq 8.17.1 pinned to version 8.17.1
coq-core 8.17.1 The Coq Proof Assistant -- Core Binaries and Tools
coq-iris dev.2024-02-05.0.a013468e A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
coq-stdlib 8.17.1 The Coq Proof Assistant -- Standard Library
coq-stdpp dev.2024-02-02.1.a2456618 An extended "Standard Library" for Coq
coqide-server 8.17.1 The Coq Proof Assistant, XML protocol server
dune 3.13.1 Fast, portable, and opinionated build system
ocaml 4.14.1 The OCaml compiler (virtual package)
ocaml-config 2 OCaml Switch Configuration
ocaml-variants 4.14.1+options Official release of OCaml 4.14.1
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
then I did
git clone https://gitlab.mpi-sws.org/iris/diaframe.git
cd diaframe/
make builddep-opamfiles
opam pin add builddep/
The last command reports an error "Missing dependency: coq >= 8.18". I nevertheless continued with
make -j 12 diaframe diaframe-heap-lang test
which quickly failed with
File "diaframe/ocaml/define_my_primitive.ml", line 8, characters 37-51:
8 | Tac2env.define_primitive (pname x) (of_closure y)
How should I setup things to be able to do make in diaframe?
from pg.
OCaml plugins are not supported, see https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General/#Current-Limitations, nevertheless I wanted to investigate, but I was not able to install diaframe.
Oh, I didn't know that. Well that is unfortunate... lucky enough things work just fine when I disable "compile before require".
How should I setup things to be able to do make in diaframe?
Seems like diaframe recently dropped support for Coq 8.17, so you'll have to update to Coq 8.18. Not sure why opam didn't do that by itself, maybe try opam install coq.8.18.0
and then again opam pin add builddep/
.
from pg.
OK, I can reproduce now.
Previously opam did not install 8.18, because I pinned 8.17, because you wrote 8.18 does not work.
Plugins being not supported means that auto-compilation does not and cannot (re-)build plugins. This would certainly hit you when you start without building or when you change a plugin. The error reported here however is a different problem.
The problem here is that coqdep
fails on diaframe/diaframe/utils_ltac2.v
. The failing coqdep
command line contains all the -Q
and -I
options from _CoqProject
, however, it does not contain any -m
option that would point coqdep
to your META file diaframe/ocaml/META.coq-diaframe
.
Can you confirm that the coqdep
command line generated by make
contains -m diaframe/ocaml/META.coq-diaframe
?
from pg.
Can you confirm that the coqdep command line generated by make contains -m diaframe/ocaml/META.coq-diaframe?
I think the answer is yes:
"coqdep" -m "diaframe/ocaml/META.coq-diaframe" -vos -dyndep var -f ._CoqProject_make > ".CoqMakefile.d" || ( RV=$?; rm -f ".CoqMakefile.d"; exit $RV )
from pg.
OK, thanks for the quick answer. Do you know if this -m
option is added automatically by coq_makefile
or if somebody did something special to get it added?
from pg.
A simple work around is to add this -m
option manually, unfortunately there was no user option in the code to do this. I added this in PR #735. Note that you have to use absolute path', because coqdep does also run in /tmp
on temp files. Best do in .dir-locals.el, eg
((nil .
((coq-compile-extra-coqdep-arguments
. ("-m" "/home/tews/coq/diaframe/diaframe/ocaml/META.coq-diaframe")))))
from pg.
OK, thanks for the quick answer. Do you know if this -m option is added automatically by coq_makefile or if somebody did something special to get it added?
No idea... the diaframe makefile contains a bunch of stuff I can't see through.
I'll try to forward this question to its author.
from pg.
Author here, I have not heard of this -m
option before, so I guess coq_makefile
adds it automatically..?
from pg.
Yes, it is difficult to find documentation about it, but coq/coq#15220 referenced in
https://coq.inria.fr/doc/V8.19.0/refman/changes.html#id579 states that coq_makefile
adds the -m
option for a META
found in _CoqProject
.
from pg.
I suggest to close this issue now in favor of #736, which is more to the point.
from pg.
Yes makes sense. Thanks for the investigation!
from pg.
Related Issues (20)
- makeinfo reports warning: @inforef is obsolete
- compile-tests/003-require-error fails sporadically with 8.19-rc1 HOT 4
- proof-goto-point is non-idempotent HOT 2
- wait for proof-goto-point to finish HOT 1
- void function error
- coq-load-project file should extract META files HOT 1
- dynamic highlighting HOT 1
- Bug: Frames in hybrid mode automatically revert to vertical mode HOT 2
- different styles of comment HOT 6
- Indentation issue : "\in" HOT 2
- 3-pane mode broken with small frame heights
- UI and kernel out of sync from aborting tactics? HOT 1
- Proof General gets into a state where it doesn't know what + is. HOT 11
- Why retracting before restarting coqtop? HOT 3
- Incompatibility with `package-quickstart` HOT 4
- bug: newlines misparsed as space in string litterals HOT 10
- File mode specification error: (void-variable coq-cmd-force-next-proof-kept) HOT 14
- REGRESSION: ProofGeneral cannot step over Fail correctly HOT 10
- PG does not position to error HOT 8
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from pg.