Shenghao Yuan (Jan 19 2021 at 16:13): Shenghao Yuan (Jan 19 2021 at 16:13):Hello,
I successfully installed the Compcert, but I hope to execute the source code of Compcert, for instance:
I hope to execute the Asm.v code from /arm, but It depends on too many other libs such as Coqlib, Maps from /lib, and they also depend on a lot of libs.
Following the suggestion from software foundation, I create the `_CoqProject` and fill in `-Q . MYFOLDER`,
I need to copy all libs and replace all CompCert libraries (e.g. `Require Import Coqlib.`) with a prefix (e.g. `From MYFOLDER Require Import Coqlib.`).
But there are too many libs, so this manual way is too ineffective, could you please give me some suggestions?
Best wishes,
Karl Palmskog (Jan 19 2021 at 16:17):just installing CompCert will not generally be helpful to checking the Coq code inside CompCert manually. You will have to build CompCert manually from scratch in a specific directory.
Guillaume Melquiond (Jan 19 2021 at 16:22):I do not understand what you mean by "executing arm/Asm.v". The only executable part of this file is the emulation of a single opcode, assuming you have a full representation of your memory already. Is that really what you want to do?
Shenghao Yuan (Jan 19 2021 at 16:57):Karl Palmskog said:
just installing CompCert will not generally be helpful to checking the Coq code inside CompCert manually. You will have to build CompCert manually from scratch in a specific directory.
Currently, I create a new folder, and copy other .v files,,, so you mean I must build them from the beginning, Does coq provide any tools to help me do that? coqmakefile?
Shenghao Yuan (Jan 19 2021 at 16:58):Guillaume Melquiond said:
I do not understand what you mean by "executing
arm/Asm.v". The only executable part of this file is the emulation of a single opcode, assuming you have a full representation of your memory already. Is that really what you want to do?
I hope to execute the Asm.v on the coqide step by step (check, more precisely)
Alix Trieu (Jan 19 2021 at 16:58):You can ./configure and make to build CompCert.
Karl Palmskog (Jan 19 2021 at 17:00):Shenghao Yuan said:
Currently, I create a new folder, and copy other .v files,,, so you mean I must build them from the beginning, Does coq provide any tools to help me do that? coqmakefile?
CompCert is very difficult to build by copying files around. Using the bundled configure script and makefile is highly recommended.
Guillaume Melquiond (Jan 19 2021 at 17:01):Yes, just do a plain compilation of CompCert, e.g., ./configure armeb-eabi && make and then you can do coqide arm/Asm.v to execute it step by step.
Shenghao Yuan (Jan 19 2021 at 17:01):Guillaume Melquiond said:
Yes, just do a plain compilation of CompCert, e.g.,
./configure armeb-eabi && makeand then you can docoqide arm/Asm.vto execute it step by step.
thx, I will try it tomorrow !!! And return the feedback :grinning:
Shenghao Yuan (Jan 19 2021 at 17:04):Alix Trieu said:
You can ./configure and make to build CompCert.
thx
Shenghao Yuan (Jan 20 2021 at 10:38):Guillaume Melquiond said:
Yes, just do a plain compilation of CompCert, e.g.,
./configure armeb-eabi && makeand then you can docoqide arm/Asm.vto execute it step by step.
It works! I spent the whole morning to make sure that coq, coqide and ocaml has the right version (I suggest to use opam instead of brew in MacOS):
- coqc -v
The Coq Proof Assistant, version 8.12.0 (January 2021)
compiled on Jan 20 2021 10:12:04 with OCaml 4.10.0
- coqide: 8.12.0
- ocaml -version
The OCaml toplevel, version 4.10.0
Last updated: Oct 13 2024 at 01:02 UTC