search

ku-fpg / hermit-shell

HERMIT with GHCi shell
BSD 3-Clause "New" or "Revised" License
2 stars 0 forks source link

Port tests #7

Open andygill opened 9 years ago

andygill commented 9 years ago

Port all tests to the new shell.

ecaustin commented 9 years ago

I believe that all of the old examples are now ported over. The only remaining uses of eval in the new examples are due to issue https://github.com/ku-fpg/hermit-shell/issues/16, e.g. `eval "rule-to-lemma ..."

roboguy13 commented 9 years ago

I ported over the hanoi example as well, which wasn't working in the original hermit setup. If someone more experienced could take a look at it to make sure I didn't break anything important in that example, I'd appreciate it. One thing in particular is that I'm not sure why an assume is necessary, what lemma it's assuming and, as a result of that, how to replace it with an explicit proof. I did see that using the hanoi hermit-shell script as it stands now has a noticeable speedup over just compiling with GHC directly, which is probably a good sign.

xich commented 9 years ago

@roboguy13 what commands do I type to run the hanoi example in hermit-shell? I can look at it and tell you if it looks correct.

unfoldRuleR introduces an obligation to prove the rule being used if it hasn't been already proven. That is why you need an assume. The fact that it isn't in the original hss script shows how long it has been since anyone ran that example. :-P

Also, curious what you mean by speedup. In the transformation time or in the runtime of the transformed program?

roboguy13 commented 9 years ago

@xich Cool, thanks! To execute the hermit-shell transformation and generate the executable for the hanoi example, run hermit-shell Hanoi.hs +Main HanoiScript.hs. After all the processing is done and you get a prompt, type :resume.

By speedup, I mean the runtime of the transformed program.

xich commented 9 years ago

Also also, the reason hanoi wasn't in the test suite previously is that it strangely would cause an endless loop and hang the test suite. This was pretty early in HERMIT's life, so it's possible some fix over the last year or so means that is no longer the case... it just never got added back to the suite.