Anish Tondwalkar

I suspect this is a special case of #221

hmm, I'm not sure what the differences are between marionette and geckodriver, but trying out selenium+geckodriver in the python repl (as per https://www.selenium.dev/documentation/en/webdriver/keyboard/) I can control vimperator from python. Narrowing...

NB this requires patching the coq haskell extraction plugin, since it still depends on ghc 8, even in the coq master branch (should be a 1-2 line patch, though)

Might be worth looking into the tools by Ringer et al --- their motivating example is typically lifting proofs about lists to vectors On Mon, Apr 12, 2021 at 7:29...

For the lack of a better constraint to blame, I'm just going to blame all of the defining constraints

This is really strange. I'm able to reproduce this on `goto` and on my machine. It has nothing to do with `z3`; all the tests are failing with error 127...

Ah, I see, `cabal install` doesn't drop `fixpoint` into `dist/build/fixpoint`. Need to run `cabal build` for that. `make` doesn't run the tests, and `make test` complains: ``` ± make test...

@peti how is the nix expression you're using on hydra created? is it simply cabal2nix? I can reproduce with ``` cabal2nix --shell . > shell.nix nix-build shell.nix ``` somehow we...

Hmm this seems to be related to nix permissions somehow? ``` $ bash

shouldn't this code be: ```haskell evalIte' γ _ b e1 e2 thenTaken elseTaken = do e1'