search

antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

make -C base breaks #94

Closed rsnikhil closed 6 years ago

rsnikhil commented 6 years ago

I'm following the directions in the README. For 'make -C base', after COQC GHC/Types.v, while processing COQC GHC/Priv.v, I get:

File "./GHC/Prim.v", line 33, characters 11-12: Syntax error: [Prim.identref] expected after [constr:global] (in [record_field_declaration]). Makefile:313: recipe for target 'GHC/Prim.vo' failed make[1]: *** [GHC/Prim.vo] Error 1 make[1]: Leaving directory '/home/nikhil/GitHub/hs-to-coq/base'

nomeata commented 6 years ago

What is your version of Coq?

rsnikhil commented 6 years ago

Ok, thanks for that question, which prompted me to investigate, and resolve that, and get further.

I had followed the 'opam' instructions earier in the README and it reported that it was installing coq.8.7.2. However, it looks like there was an earlier installation of Coq on my computer, and that version was still getting picked up. I resolved that, and now 'make -C base' and 'base-thy' complete successfully.

Now when I try running hs-to-coq, I'm getting messages like this: Could not find GHC/Types.h2ci in any of these directories: Please either process GHC.Types first, or skip declarations that mention GHC.Types. and I'm trying to figure out what exactly that means and how to resolve it.

Thanks.

nomeata commented 6 years ago

That error is not critical, I think. Can you run the base-tests?

nomeata commented 6 years ago

Or rather: what are you trying to do?

nomeata commented 6 years ago

Alepy, how are you trying to run it? It's easiest to base your experiments on the examples, e.g. examples/succsessors, including the Makefile setup there

rsnikhil commented 6 years ago

Or rather: what are you trying to do? How are you trying to run it?

High level goal: I have written a formal semantics for the RISC-V ISA, in Haskell (*), which is in:

https://github.com/rsnikhil/RISCV-ISA-Spec

It's pretty extensive (it boots the Linux kernel), covering both RV32 and RV64; Machine, Supervisor and User privilege levels; Sv32, Sv39 and Sv48 virtual memory schemes; standard extensions for Integer Multiply/Divide and Atomics, and soon to include Floating Point and Compressed instructions.

I'm playing around with importing it into Coq so that I can reason about it in Coq (I'm new to Coq, so I'm also using this to learn Coq). I'm applying hs-to-coq like so, following the directions in hs-to-coq's README:

$ stack exec hs-to-coq -- -o TMP_OUT/ --import-dir ~/GitHub/RISCV-ISA-Spec/src  ~/GitHub/RISCV-ISA-Spec/src/Forvis_Spec.hs

It seems to succeed with no problem in translating all the files rooted at the one I provide, except for messages like "Could not find GHC/Types.h2ci in any of these directories" I cited earlier. As you say, these may be benign.

(*) There are two other attempts (that I know of) to formalize RISC-V ISA semantics in Haskell, one by Adam Chlipala's group at MIT:

https://github.com/mit-plv/riscv-semantics ) in

and one by Ben Selfridge at Galois:

https://github.com/GaloisInc/grift

My approach differs from those in at least the following ways:

(1) I have deliberately gone in the direction of 'extremely elementary Haskell' for the widest possible audience (many in the RISC-V community have no knowledge of FPLs and Haskell and some may even be intimidated by it). No monads, no typeclasses, no GADTs, no ghc extensions, nothing, just functional programming 101 (it ought to be a breeze for hs-to-coq!)

(2) I have a different approach to modeling concurrency, needed to properly model pipelining, out-of-order execution, speculation, and interaction with weak memory models.

nomeata commented 6 years ago

Cool project. Are you saying that you have a hardware simulator in Haskell that is good enough to boot Linux? How slow is that?

Maybe we should have a chat session to get you started. Are you around this afternoon?

nomeata commented 6 years ago

Maybe Skype or Meet or something with screen sharing

rsnikhil commented 6 years ago

Yes, I have a RISC-V simulator in Haskell that boots the LInux kernel. I'll be happy to chat with you. I'm in a meeting just now (2pm EDT onwards), not sure when it will end (hopefully by 3pm). I can ping you after that and send you a zoom invite. (PS: had a long chat with Antal some months ago about hs-to-coq). You can send me email directly at: nikhil AT acm.org

sweirich commented 6 years ago

I'm going to close this issue with just a link to the RISC-V repository: https://github.com/rsnikhil/RISCV-ISA-Spec/tree/master/verification