Leonhard Markert

Two questions at this point: 1. The fact that counterexamples come so easily makes me wonder if `expr == rr (showpp expr)` is even a goal -- is it? 2....

@ranjitjhala that makes sense. In that case I suggest closing this ticket. Can you think of uses for an `instance Arbitrary Expr`? I revived / rewrote it for experimenting on...

Disclaimer: I haven't contributed for long, so I may have gotten this wrong. # Existing parsers and pretty-printers I count four pairs of parsers and pretty-printers in `liquid-fixpoint`. ## FQ...

> Of the three parsers that remain, two of them use the third one, right? FQs and Horn queries depend on the parser of Expressions to, well, parse expressions. Thanks,...

For completeness' sake, here are two more types with parsers attached to them. ## SMT command - Type: [`Smt.Types.Command`](https://github.com/ucsd-progsys/liquid-fixpoint/blob/3438be3ddf1823aab84b47b0ad34f03640ea384c/src/Language/Fixpoint/Smt/Types.hs#L47-L62) (several constructors take an `Expr`). - Parser: [`Parse.commandP`](https://github.com/ucsd-progsys/liquid-fixpoint/blob/3438be3ddf1823aab84b47b0ad34f03640ea384c/src/Language/Fixpoint/Parse.hs#L1506-L1513). - Pretty-printer (SMTLIB2):...

> How would you arrange things otherwise? My starting point is that any hand-written parser and pretty-printer needs maintenance and testing. So looking at the situation holistically, my aim would...

> As it happens there is a fifth one: Horn.Parse :-) Is this one different from [what I called "SMT2 files"](https://github.com/ucsd-progsys/liquid-fixpoint/issues/46#issuecomment-972704494), parsed by `Horn.Parse.hornP`? (I edited that comment several times...

Since May 9th, there have been two Hackage releases of `liquid-fixpoint`: - https://hackage.haskell.org/package/liquid-fixpoint-8.10.7 on 2021-11-03 - https://hackage.haskell.org/package/liquid-fixpoint-0.8.10.7 on 2021-11-05 So it looks like the fixes have been released and this...

This should be fixed by https://github.com/ucsd-progsys/liquid-fixpoint/pull/509.

> hydra Ah, right. For the record, `liquid-fixpoint-0.8.10.2` and `liquid-fixpoint-8.10.7` are part of Nixpkgs `master`: https://github.com/NixOS/nixpkgs/blob/3e8ff3181b754e4646766849b5e8142406ac3f12/pkgs/development/haskell-modules/hackage-packages.nix And at least on some branches of Nixpkgs, builds are taking place: https://hydra.nixos.org/job/nixos/release-21.05/nixpkgs.haskellPackages.liquid-fixpoint.x86_64-linux Unfortunately...