Problems with Coq

[amelieled]

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]

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]

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]

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.