search

rems-project / lem

Lem semantic definition language
Other
130 stars 15 forks source link

Problems with Coq #30

Closed amelieled closed 1 year ago

amelieled commented 4 years ago

Hi everyone! I'm trying to test the features of Lem linking to Coq. My version of Coq is 8.10.2 (June 2020) but I obtained this error when I executed the command Require Import coqharness. (file lem_list.v): The file ~/lem/coq-lib/coqharness.vo contains library Lem.coqharness and not library coqharness

And why have I a lot of (* [?]: removed value specification. *) and (* [?]: removed top-level value definition. *) generated automatically? Moreover, the function length is in comment but I don't understand why.

Thanks!

bacam commented 1 year ago

Probably far too late, but nonetheless ...

To import the library you need to tell Coq how to map the library name Lem to the directory where the files are, e.g., coqide -R <path to coq-lib> Lem .... The reason for all the comments is that the source Lem library files declare mappings to native Coq functions. For example, length is mapped to List.length in the Coq output of any Lem file that uses it, so the library file doesn't need a definition.

amelieled commented 1 year ago

It is never too late. So thanks.

There is somewhere in the document which explains that? Do you plan to add a CI on this project?

bacam commented 1 year ago

I'm not sure how well documented the Coq backend is; it isn't used much because the Lem language isn't a great match for Coq.

I don't have any CI plans (although perhaps we should dig out whatever we used to use in Jenkins), although there are some basic self-tests that are run whenever the OCaml libraries are built. I think the tests in the Makefile have bitrotted somewhat.