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

hs-to-coq goes into a seeming infinite loop with memory explosion #112

Closed jwiegley closed 4 years ago

jwiegley commented 6 years ago

  1. git clone https://github.com/SPY/haskell-wasm

  2. cd haskell-wasm

  3. Use the following edits file:

rename type Data.ByteString.Lazy.Internal.ByteString = Coq.Strings.String.string
rename type Data.Text.Internal.Lazy.Text = Coq.Strings.String.string
rename type GHC.Natural.Natural = Coq.Numbers.BinNums.N
rename value Language.Wasm.Structure.MemArg = Language.Wasm.Structure.MkMemArg
rename value Language.Wasm.Structure.Limit = Language.Wasm.Structure.MkLimit
  1. Run the following command:
hs-to-coq -e /Users/johnw/src/plclub/hs-to-coq/base/edits -e edits --iface-dir ~/src/plclub/hs-to-coq/base -i src src/Language/Wasm/Structure.hs > Structure.v

It's just like crypocurrency mining, just without making any money!

emarzion commented 6 years ago

Just thought I'd chime in and say that I've had memory issues as well when translating code involving large pattern matches, and I believe the culprit is isCompleteMultiPattern. I was able to disable this (it's only invoked twice in Expr.hs) and the memory issues have gone away.

nomeata commented 6 years ago

That’s my code, and I would not be surprised if I walk right into some combinatorial explosion while doing pattern exhaustiveness checks – after all, there are whole papers written about that…

trommler commented 4 years ago

With #146 applied the above file is translated in under a second using under 200 KB of memory on my machine.