clarus / coq-chick-blog Goto Github PK

Using coq 8.5 beta2 (which got installed when using opam, compilation failed in src/Extraction.v:

"coqc"  -q  -R "src" ChickBlog   src/Extraction
File "./src/Extraction.v", line 98, characters 0-1002:
Error: Cannot guess decreasing argument of fix.
make: *** [src/Extraction.vo] Error 1

I'm an absolute beginner at coq so can't help much further.

Apologies if I'm missing something silly. I'm learning Coq and wanted to play around with this some, but it seems to not be able to find cohttp.lwt even though it appears to be installed.

ricky@t520 99% /tmp/coq-chick-blog/extraction (master)$ opam install --jobs=4 lwt cohttp
[NOTE] Package lwt is already installed (current version is 2.4.5).
[NOTE] Package cohttp is already installed (current version is 0.11.2).

ricky@t520 99% /tmp/coq-chick-blog/extraction (master)$ make
ocamlbuild chickBlog.native -use-ocamlfind -package cohttp.lwt,lwt,lwt.unix,num,str
+ ocamlfind ocamldep -package cohttp.lwt,lwt,lwt.unix,num,str -modules chickBlog.ml > chickBlog.ml.depends
ocamlfind: Package `cohttp.lwt' not found
Command exited with code 2.
Compilation unsuccessful after building 1 target (0 cached) in 00:00:00.
Makefile:2: recipe for target 'build' failed
make: *** [build] Error 10

Your project is extremely interesting to me, as the aspects it touches on are exactly what I want to learn with using Coq.

Right now I'm trying to step through Spec.v using CoqIDE, but it can't find Computation.vos. Why, I have no clue, because I've compiled the source files using configure.sh && make.

Here is a screenshot:

In your README it would be nice to mention you need to download the other projects you've written (coq-moment, coq-list-strings, etc) 🙂 I can make a PR for this.

All in all, awesome work. I think it's a fantastic piece to learn from. How long have you been using Coq before you wrote this?