search

atlanmod / coqtl

CoqTL allows users to write model transformations and prove engine/transformation correctness in Coq
Other
13 stars 12 forks source link

Unable to make the project #73

Closed luntan-maker closed 2 years ago

luntan-maker commented 4 years ago

Hello,

I've spent a little while trying to figure out how to get the master branch up and going, and I have no clue at this point. Good news, I've been able to get the jscoq branch to work. I've copy-pasted four sections general system information, making the jscoq branch, and two variations of making the master branch. Any advice would be wonderful, and please let me know if I can get any other information for you.

coqc --version The Coq Proof Assistant, version 8.6 (June 2020) compiled on Jun 23 2020 13:4:17 with OCaml 4.05.0

make --version GNU Make 4.1 Built for x86_64-pc-linux-gnu Copyright (C) 1988-2014 Free Software Foundation, Inc. License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html> This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law.

cat /etc/os-release NAME="Ubuntu" VERSION="18.04.4 LTS (Bionic Beaver)" ID=ubuntu ID_LIKE=debian PRETTY_NAME="Ubuntu 18.04.4 LTS" VERSION_ID="18.04" HOME_URL="https://www.ubuntu.com/" SUPPORT_URL="https://help.ubuntu.com/" BUG_REPORT_URL="https://bugs.launchpad.net/ubuntu/" PRIVACY_POLICY_URL="https://www.ubuntu.com/legal/terms-and-policies/privacy-policy" VERSION_CODENAME=bionic UBUNTU_CODENAME=bionic

git clone -b jscoq https://github.com/atlanmod/CoqTL.git cd CoqTL make

COQDEP theories/test/Class2Relational/Class2Relational_test.v COQDEP theories/test/Class2Relational/Class2Relational.v COQDEP theories/test/Class2Relational/PersonModel.v COQDEP theories/test/Class2Relational/RelationalMetamodel.v COQDEP theories/test/Class2Relational/ClassMetamodel.v COQDEP theories/transformation/Notations.v COQDEP theories/transformation/CoqTL.v COQDEP theories/transformation/Engine.v COQDEP theories/transformation/Model.v COQDEP theories/transformation/Metamodel.v COQDEP theories/utils/tTop.v COQDEP theories/utils/tNotation.v COQDEP theories/utils/tPrint.v COQDEP theories/utils/tString.v COQDEP theories/utils/tTuple.v COQDEP theories/utils/tConcat.v COQDEP theories/utils/tList.v COQDEP theories/utils/tArith.v COQC theories/utils/tArith.v COQC theories/utils/tList.v COQC theories/utils/tConcat.v COQC theories/utils/tTuple.v COQC theories/utils/tString.v COQC theories/utils/tPrint.v COQC theories/utils/tNotation.v COQC theories/utils/tTop.v COQC theories/transformation/Model.v COQC theories/transformation/Metamodel.v COQC theories/transformation/Engine.v COQC theories/transformation/CoqTL.v SourceModel : Type

SourceModel is transparent Expands to: Constant coqtl.transformation.CoqTL.CoqTL.SourceModel COQC theories/transformation/Notations.v File "./theories/transformation/Notations.v", line 12, characters 0-86: Warning: This notation will not be used for printing as it is bound to a single variable. [notation-bound-to-variable,parsing] File "./theories/transformation/Notations.v", line 21, characters 0-206: Warning: This notation will not be used for printing as it is not reversible. [non-reversible-notation,parsing] COQC theories/test/Class2Relational/ClassMetamodel.v COQC theories/test/Class2Relational/RelationalMetamodel.v COQC theories/test/Class2Relational/PersonModel.v COQC theories/test/Class2Relational/Class2Relational.v COQC theories/test/Class2Relational/Class2Relational_test.v = {| Model.allModelElements := RelationalMetamodel_BuildEObject TableClass (BuildTable 0 "Person") :: RelationalMetamodel_BuildEObject ColumnClass (BuildColumn 1 "father") :: nil; Model.allModelLinks := RelationalMetamodel_BuildELink TableColumnsReference (BuildTableColumns (BuildTable 0 "Person") (BuildColumn 1 "father" :: nil)) :: RelationalMetamodel_BuildELink ColumnReferenceReference (BuildColumnReference (BuildColumn 1 "father") (BuildTable 0 "Person")) :: nil |} : TargetModel RelationalMetamodel_EObject RelationalMetamodel_ELink

git clone https://github.com/atlanmod/CoqTL.git cd CoqTL cd fr.inria.atlanmod.coqtl.coq make

coqc: --print-version: no such file or directory COQDEP VFILES coqc: --print-version: no such file or directory coqc: --print-version: no such file or directory W: This Makefile was generated by Coq 8.8.1 W: while the current Coq version is coqc: --print-version: no such file or directory COQC core/utils/tArith.v COQC core/utils/tList.v COQC core/utils/tConcat.v COQC core/utils/tTuple.v COQC core/utils/tString.v File "./core/utils/tString.v", line 2, characters 15-37: Error: Unable to locate library core.utils.CpdtTactics. Makefile:656: recipe for target 'core/utils/tString.vo' failed make[1]: [core/utils/tString.vo] Error 1 Makefile:317: recipe for target 'all' failed make: [all] Error 2

git clone https://github.com/atlanmod/CoqTL.git cd CoqTL cd fr.inria.atlanmod.coqtl.coq coq_makefile -f _CoqProject -o Makefile make

'akefile:261: warning: overriding recipe for target ' 'akefile:231: warning: ignoring old recipe for target ' 'akefile:282: warning: overriding recipe for target ' 'akefile:261: warning: ignoring old recipe for target ' 'akefile:303: warning: overriding recipe for target ' 'akefile:282: warning: ignoring old recipe for target ' 'akefile:324: warning: overriding recipe for target ' 'akefile:303: warning: ignoring old recipe for target ' COQDEP examples/HSM2FSM/HSMModel.v Warning: in file examples/HSM2FSM/HSMModel.v, library core.Model is required and has not been found in the loadpath! Warning: in file examples/HSM2FSM/HSMModel.v, library core.Model is required and has not been found in the loadpath! 'akefile:261: warning: overriding recipe for target ' 'akefile:231: warning: ignoring old recipe for target ' 'akefile:282: warning: overriding recipe for target ' 'akefile:261: warning: ignoring old recipe for target ' 'akefile:303: warning: overriding recipe for target ' 'akefile:282: warning: ignoring old recipe for target ' 'akefile:324: warning: overriding recipe for target ' 'akefile:303: warning: ignoring old recipe for target ' make: *** No rule to make target 'examples/HSM2FSM/HSM.vo', needed by 'examples/HSM2FSM/HSMModel.vo'. Stop.

veriatl commented 4 years ago

Hi

Thank you for the report. I can reproduce the error under Coq 8.6.

I must admit we lost track of readme file while we are developing CoqTL. Sorry for inconvenience.

We are currently developing on Coq 8.11.1. Here are my steps that compile CoqTL-master successfully.

cd CoqTL cd fr.inria.atlanmod.coqtl.coq git clean -fdx coq_makefile -f _CoqProject -o Makefile make

I have corrected the Coq dependency in the readme.md. Hope that works for you.

Best, Zheng

luntan-maker commented 4 years ago

Whenever I get to coq_makefile it gives me the following: Unknown option Usage summary:

coq_makefile .... [file.v] ... [file.ml[ig]?] ... [file.ml{lib,pack}] ... [any] ... [-extra[-phony] result dependencies command] ... [-I dir] ... [-R physicalpath logicalpath] ... [-Q physicalpath logicalpath] ... [VARIABLE = value] ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file] [-h] [--help]

Full list of options:

[file.v]: Coq file to be compiled [file.ml[ig]?]: Objective Caml file to be compiled [file.ml{lib,pack}]: ocamlbuild-style file that describes a Objective Caml library/module [any] : subdirectory that should be "made" and has a Makefile itself to do so. Very fragile and discouraged. [-extra result dependencies command]: add target "result" with command "command" and dependencies "dependencies". If "result" is not generic (do not contains a %), "result" is built by make all and deleted by make clean. [-extra-phony result dependencies command]: add a PHONY target "result" with command "command" and dependencies "dependencies". Note that -extra-phony foo bar "" is a regular way to add the target "bar" as as a dependencies of an already defined target "foo". [-I dir]: look for Objective Caml dependencies in "dir" [-R physicalpath logicalpath]: look for Coq dependencies recursively starting from "physicalpath". The logical path associated to the physical path is "logicalpath". [-Q physicalpath logicalpath]: look for Coq dependencies starting from "physicalpath". The logical path associated to the physical path is "logicalpath". [VARIABLE = value]: Add the variable definition "VARIABLE=value" [-byte]: compile with byte-code version of coq [-opt]: compile with native-code version of coq [-arg opt]: send option "opt" to coqc [-install opt]: where opt is "user" to force install into user directory, "none" to build a makefile with no install target or "global" to force install in $COQLIB directory [-f file]: take the contents of file as arguments [-o file]: output should go in file file (recommended) Output file outside the current directory is forbidden. [-h]: print this usage summary [--help]: equivalent to [-h]

Here is a dockerfile that reproduces the output.

Thank you for your time, Lucas.

veriatl commented 4 years ago

Hi Lucas,

could you try to move to the flat-syntax-parametric branch to see whether the problem persists?

ps: I think the _CoqProject in the master branch is created under windows, and not compatible with Linux (some format thing I guess). If you create a new file, with the same content, it should do the trick. I'll see how it should be updated in the coming days.

Cheers, Zheng

luntan-maker commented 4 years ago

Hi Zheng,

Logs for master, logs for flat-syntax-parametric. The _CoqProject file was local, I just copy-pasted from the GitHub repo into a text editor and saved it. There still seems to be problems with the master branch, although the flat-syntax-parametric branch seems to work just fine.

Thank you for your time, Lucas.