Gabriel Ebner

BTW, the s-expression parser is pretty small. We could easily switch to another parsing library if that simplifies anything, as long as the performance remains reasonable.

I'm not sure that would work. Z3 doesn't output empty lines after every response.

As a first step, it would probably be a good idea to rework the existing veriT interface to use our s-expression parser, see #563.

Ah, looks like erasure reduction does not handle Skolemization. As a quick fix you could start with `CNFReductionExpRes` instead, then the further reductions will not see the strong quantifiers.

I have done some performance tests with Lists vs. Vectors in [trepplein](https://github.com/gebner/trepplein) and was pleasantly surprised by the performance of Vector. I think we should go ahead with this change,...

I've now put in a fix based on solution 1. It was a bit more complicated than expected, you need to add only the free variabkes, otherwise you get an...

Related: [Smolka, Blanchette: Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs](http://www.easychair.org/publications/download/Robust_Semi-Intelligible_Isabelle_Proofs_from_ATP_Proofs) They take a somewhat similar approach to proof import as we do: inferences are treated as first-order consequences and reconstructed...

I certainly have no objections to changing the error message. > should we store the lakefile loading error in `LAKE_INVALID_CONFIG` so that we can show it instead of this generic...

I just ran into this again. > It does not seem feasible to store the entire stderr of either the configuration file elaboration or Lake itself in the environment variable....

Shake can do that. The standard example of compiling a C file looks like this: ```haskell "_build//*.o" %> \out -> do let c = dropDirectory1 $ out - "c" let...