search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
133 stars 60 forks source link

parse . pprint != id #46

Open gridaphobe opened 9 years ago

gridaphobe commented 9 years ago

See https://github.com/ucsd-progsys/liquid-fixpoint/blob/master/tests/test.hs for a failing quickCheck property.

ranjitjhala commented 9 years ago

Can you create a few concrete checks that fail so that we don't have to run quick check to get them?

On Feb 8, 2015, at 11:19 AM, Eric Seidel notifications@github.com wrote:

See https://github.com/ucsd-progsys/liquid-fixpoint/blob/master/tests/test.hs for a failing quickCheck property.

— Reply to this email directly or view it on GitHub.

gridaphobe commented 9 years ago

Hrm, something's fishy here, upon closer inspection

λ> let e = (EApp "Set_mem" [EVar "x", EApp "keys" [EVar "y"]])
e :: Expr
λ> showpp e
"(Set_mem x (keys y))"

and yet, LH renders the same expression as Set_mem x keys y... Note that even the outer parens are missing, do we have a separate pretty-printer in the LH repo??

spinda commented 9 years ago

Yes we do. LH's PPrint instance for Expr is in Types.hs. It was originally in PrettyPrint.hs, where it was introduced in this commit, a week before the one that introduced pretty-printing to liquid-fixpoint. They're the same, except that this LH commit removed the parens that you refer to; the same change wasn't made to the pretty-printer in liquid-fixpoint.

ranjitjhala commented 9 years ago

Thanks! Yes, this will make it a lot easier to fix this issue...

On Fri, Feb 13, 2015 at 1:31 AM, Michael Smith notifications@github.com wrote:

Yes we do. LH's PPrint instance for Expr is in Types.hs https://github.com/ucsd-progsys/liquidhaskell/blob/master/src/Language/Haskell/Liquid/Types.hs#L1334. It was originally in PrettyPrint.hs, where it was introduced in this commit https://github.com/ucsd-progsys/liquidhaskell/commit/4545d7c30be92dbb9156843e9fe5a99804e0c882, a week before the one that introduced pretty-printing to liquid-fixpoint https://github.com/ucsd-progsys/liquid-fixpoint/commit/5616c1253ed6d245349c34985361d512866b3018. They're the same, except that this LH commit https://github.com/ucsd-progsys/liquidhaskell/commit/2c8af7b2b09670310c0f227e791b85c0b01b1651#diff-7be711f18ea48ead1cbe08cedb81dfaeR1250 added the parens removal that you refer to, but the same change wasn't made to the one in liquid-fixpoint.

Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquid-fixpoint/issues/46#issuecomment-74227056 .

Ranjit.

ranjitjhala commented 9 years ago

@gridaphobe -- do you think you can take a crack at this after your RE? Should be easy?

gridaphobe commented 9 years ago

@spinda thanks for digging around! I'll look into a fix next week.

curiousleo commented 2 years ago

I'm taking a look at this today.

curiousleo commented 2 years ago

I revived / rewrote some of the Arbitrary instances already present in tests/test.hs. At the top level, expressions are generated and we check the following:

expr == rr (showpp expr)

In doing so, I've come across a few parsing errors and a few instances where the equality fails. Note that I am probably not validating expressions properly -- some or all of these may not actually be considered valid expressions.

Parsing errors

Some expressions lead to parsing errors:

PGrad $"symbol"  (GradInfo {..}) (ECon (I 0))

            |                                                                                                                                                            
          1 | 0 && $symbol                                                                                                                                               
            |   ^                                                                                                                                                        
          unexpected '&'                                                                                                                                                 
          expecting "mod", '*', '+', '-', '.', '/', or end of input}]
PImp (EVar "symbol") (ECon (R 0.0))

            |
          1 | symbol => 0.0
            |        ^
          unexpected '='
          expecting "mod", '*', '+', '-', '.', '/', or end of input}]
PIff (ESym (SL "j")) (EVar "symbol")

            |
          1 | "j" <=> symbol
            |     ^
          unexpected '<'
          expecting "mod", '*', '+', '-', '.', '/', or end of input}]
ECoerc (FVar (-1)) (FApp FReal FInt) (ECon (I 0))

            |
          1 | (coerce @(-1) ~ (real int) in 0)
            |         ^
          unexpected '@'
          expecting '(' or '-'}]
ECoerc (FApp FReal FInt) (FApp FInt FInt) (ESym (SL "xp"))

            |
          1 | (coerce (real int) ~ (int int) in "xp")
            |                  ^
          unexpected ')'
          expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", '(', '-', '@', '[', '~', lowerIdP, or uppercase letter}]
PAll [("rhi",FFunc FReal FInt),("sq",FVar (-1))] (ESym (SL "sgki"))

            |
          1 | forall [rhi : func(0 , [real; int]); sq : @(-1)]
            |       ^
          unexpected reserved word "forall"}]
ELam ("gov",FApp FFrac FInt) (ESym (SL "jum"))

            |
          1 | lam gov : (frac int) . "jum"
            |         ^
          unexpected ':'
PAnd [PAnd [ECon (I 0),POr [EVar "bhk",ECon (I 0)]],ESym (SL "l")]

            |                                                                                                                                                            
          2 |  && (bhk                                                                                                                                                   
            |  ^^                                                                                                                                                        
          unexpected "&&"                                                                                                                                                
          expecting "::", "mod", ')', '*', '+', ',', '-', '.', '/', or ':'}]

showpp gives:

(0
 && (bhk
     || 0))
&& "l"

Not inverses

Other expressions are parsed successfully, but into a different expression than the original:

  PNot (ESym (SL "ogdr"))

showpp ==>
  not "ogdr"
rr . showpp ==>
  EApp (EVar "not") (ESym (SL "ogdr"))
  ETAbs (EVar "symbol") "symbol"

showpp ==>
  ETAbs symbol symbol
rr . showpp ==>
  EApp (EApp (EVar "ETAbs") (EVar "symbol")) (EVar "symbol")
  ECon (L "t" (FAbs 0 FFrac))

showpp ==>
  (lit "t" func(1 , [frac]))
rr . showpp ==>
  ECon (L "t" (FAbs 0 (FObj "frac")))
curiousleo commented 2 years ago

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. Do you see anything obviously wrong with the generated expressions in the counterexamples, that is, are any of them invalid? I would try to add validation so invalid expressions are not generated.
ranjitjhala commented 2 years ago

TBH while the goal seems good, I think it may be too hard at this point I especially worry if there are changes to the parser that will break a lot of stuff :-(

On Tue, Nov 16, 2021 at 7:57 AM Leonhard Markert @.***> wrote:

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. Do you see anything obviously wrong with the generated expressions in the counterexamples, that is, are any of them invalid? I would try to add validation so invalid expressions are not generated.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_46-23issuecomment-2D970413108&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=X8tiycoxqo3NhG3bpuavDvNhcaoebSPpE1C8jjv9ghZvGPjJIIF7pGNKCHWEueWs&s=53PCDIs6kIUhLILp4yzHwd6zeZhD3WrHbQsVpN1twN8&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OGATFE2CXIZ6KLLQ3LUMJ5MNANCNFSM4A3VWEMQ&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=X8tiycoxqo3NhG3bpuavDvNhcaoebSPpE1C8jjv9ghZvGPjJIIF7pGNKCHWEueWs&s=TMlEeeb6RpmiOLc8BTwRzhMBJ0bfzNdtmjHumlqCu5k&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=X8tiycoxqo3NhG3bpuavDvNhcaoebSPpE1C8jjv9ghZvGPjJIIF7pGNKCHWEueWs&s=-oVhp9BYhBED7P41SEX2rSvVLTBMccn3o_XfB_Nzx-o&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=X8tiycoxqo3NhG3bpuavDvNhcaoebSPpE1C8jjv9ghZvGPjJIIF7pGNKCHWEueWs&s=vUruKqYjn4l3P2n7MwRTeRE2ITYggNENAO1wvX23nEs&e=.

curiousleo commented 2 years ago

@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 this issue and created a draft PR for it here: https://github.com/ucsd-progsys/liquid-fixpoint/pull/513. I would like to include at least one test in that PR that actually makes use of the Arbitrary Expr instance.

facundominguez commented 2 years ago

I have found cases where liquid-fixpoint would be unable to read the very same .fq files that it has produced. At this stage, I can go and fix it for my particular case, but this is rather unergonomic. It would give us a better debugging experience if the round-trip property held.

I especially worry if there are changes to the parser that will break a lot of stuff :-(

We could avoid that by fixing the pretty-printer instead, or by strictly expanding the set of strings accepted by the parser.

@ranjitjhala, just so I have more context, who is currently depending on the parser? IIUC liquidhaskell doesn't use it.

ranjitjhala commented 2 years ago

@facundominguez -- yes I agree, its annoying to have generated .fq files that don't parse. I wonder if we can make some small examples that we can use to fix this issue instead? liquidhaskell does use some parts, e.g. the parsers for Sort, Expr / Pred, Qualifier and some other such things, so we probably don't want to change those.

But yes, there are lots of little things that the pretty-printer "breaks" parsing wise that we can fix instead.

One possibility:

  1. rerun just the liquid-fixpoint tests but with --save on so we emit the .fq files,
  2. see which of those files fail to parse
  3. see if we can update the pretty-printer/parser so that the above "round-trip" passes?
facundominguez commented 2 years ago
  1. see which of those files fail to parse

That could help too. Are you trying to avoid using quickcheck for some reason? I would expect quickcheck to be rather effective at discovering failing cases.

ranjitjhala commented 2 years ago

Hmm good point! I thought the failing tests might more quickly pinpoint the specific problems that need to be addressed to solve your issue of not being able to parse generated FQ files?

On Tue, Nov 16, 2021 at 12:49 PM Facundo Domínguez @.***> wrote:

  1. see which of those files fail to parse

That could help too. Are you trying to avoid using quickcheck for some reason? I would expect quickcheck to be rather effective at discovering failing cases.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_46-23issuecomment-2D970666412&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=H3Fviyy1URXn58Dg_NRuPcMS1sj5Yzi86FqwJEb70190PbwuizxleBFp6Aia-hcz&s=NqsI6g8ZMVDR0yp3abl0rBxWf1eXGz0Vb21s2V7E4RQ&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OFF4PR2GBMR4HURJKDUMK7TVANCNFSM4A3VWEMQ&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=H3Fviyy1URXn58Dg_NRuPcMS1sj5Yzi86FqwJEb70190PbwuizxleBFp6Aia-hcz&s=Ed0bHYn8Vyg7lBCm5ozbj6KlXA4q1lUPDBOTUukDApU&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=H3Fviyy1URXn58Dg_NRuPcMS1sj5Yzi86FqwJEb70190PbwuizxleBFp6Aia-hcz&s=UEnBLikLKC4DTTR3plr055L5M6BZSwvHlLS7_iydph4&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=H3Fviyy1URXn58Dg_NRuPcMS1sj5Yzi86FqwJEb70190PbwuizxleBFp6Aia-hcz&s=E3CvTPlHVELqOYnoP9a3tZfriPu252zOq6n6vSILZds&e=.

facundominguez commented 2 years ago

I thought the failing tests might more quickly pinpoint the specific problems that need to be addressed to solve your issue of not being able to parse generated FQ files?

Yes. I think that those tests will help exposing issues for which quickcheck would need a lot of arbitrary instances. But quickcheck can explore better the round trip for those types which do have arbitrary instances today. In sum, probably doing both is worth the trouble.

ranjitjhala commented 2 years ago

👍🏽 Agreed!!

On Wed, Nov 17, 2021 at 4:34 AM Facundo Domínguez @.***> wrote:

I thought the failing tests might more quickly pinpoint the specific problems that need to be addressed to solve your issue of not being able to parse generated FQ files?

Yes. I think that those tests will help exposing issues for which quickcheck would need a lot of arbitrary instances. But quickcheck can explore better the round trip for those types which do have arbitrary instances today. In sum, probably doing both is worth the trouble.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_46-23issuecomment-2D971537996&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=OLqYvWRGuiYpqOvlq7Ockrf_uv7MIQAYfV1_O-jWXXvMjZa8qAZiVxRVksI6yzj0&s=5sx72wxrvH1z7RJGqCE5-0Ra4G7wJ96F7zkzJbx1p_M&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OH3FLJ7ISZQZGBXLATUMOONVANCNFSM4A3VWEMQ&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=OLqYvWRGuiYpqOvlq7Ockrf_uv7MIQAYfV1_O-jWXXvMjZa8qAZiVxRVksI6yzj0&s=OoS1oscrbl6m-ug8tYyVqYwQ83gBXgZlUGA9DwpRguw&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=OLqYvWRGuiYpqOvlq7Ockrf_uv7MIQAYfV1_O-jWXXvMjZa8qAZiVxRVksI6yzj0&s=9uXJ-w53ij866gR5WWSOR8X7CqCAJiCVe36qQjcVc3E&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=OLqYvWRGuiYpqOvlq7Ockrf_uv7MIQAYfV1_O-jWXXvMjZa8qAZiVxRVksI6yzj0&s=NDkqaisDEsJvg1ww9mj4QFQ3Q-MOxo1kWL3OHcM8uAQ&e=.

curiousleo commented 2 years ago

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 files

BFQ files

SMT2 files

Expressions

Scope of this ticket

My understanding is that this ticket was originally about the expression parser and pretty-printer. The original code linked to generates expressions Expr (and also predicates Pred, but type Pred = Expr so I have not listed them separately above).

I have found cases where liquid-fixpoint would be unable to read the very same .fq files that it has produced.

This is also a parsing / pretty-printing issue, but it's about the FQ parser and pretty-printer. So perhaps it should be tracked in a separate ticket.

On the other hand: four more or less independent parser/pretty-printer pairs seems like a lot. Granted, the BFQ pair is derived, which is nice. But three pairs is still a lot. Perhaps more of them could be derived.

Expr needs a parser because expressions are written by humans. All the other formats are just LH talking to itself, as far as I can tell. The text formats FQ and SMT2 are additionally meant to make at least some sense to LH developers.

facundominguez commented 2 years ago

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. Thus, they aren't three separate parsers. Does this fact make the implementation more sensible? How would you arrange things otherwise?

curiousleo commented 2 years ago

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, that clarifies the connection: for the FQ parser / pretty-printer to be inverses of each other it is necessary but not sufficient that the Expression parser / pretty-printer are inverses of each other.

curiousleo commented 2 years ago

For completeness' sake, here are two more types with parsers attached to them.

SMT command

SMT response

ranjitjhala commented 2 years ago

As it happens there is a fifth one: Horn.Parse :-)

the smt pair is specialized to SMTLIB hence has to be different.

curiousleo commented 2 years ago

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 be to reduce parsing and pretty-printing code as much as possible.

Languages that need custom parsing or pretty-printing

Expression

The Expression (Expr) language is a custom language and needs its own parser. Given that the Expression language is used inside the FQ and Horn languages, its pretty-printer needs to be reversible and that needs to be tested.

Proposal: keep parser and pretty printer and test them.

SMT commands and responses

SMT commands and responses also form their own language that is specified elsewhere. I have not looked into it much, but perhaps we can use smtlib2 here? That way LH doesn't have to maintain its own parser and pretty-printer for this.

Proposal: evaluate smtlib2.

Internal languages

If I understood things correctly, the FQ, BFQ and SMT2 file formats are internal to LH (although some SMT2 files say "TODO move to actual SMTLIB format"), so we have full freedom here.

Binary formats can be compact, fast to write and read, so BFQ (or something like it) should stay.

But there is value in having a human readable form of these too. A simple and fast way to get human-readable invertible pretty-printing would be to use aeson to serialise to and deserialise from JSON.

Note that if a standard serialisation method like aeson is used for FQ and SMT2 files, I would suggest serialising Expressions contained in them using the same method (rather than using the custom Expression pretty-printer). If we do this then we may not even need a reversible custom pretty-printer for Expression at all.

(The counter-argument here may be that it is weird to serialise what are essentially programs to JSON, which looks like a data serialisation format. So S-expressions may be the way to go for FQ and SMT2 (SMT2 is already mostly S-expressions, except for the Expression sub-language). Unfortunately I'm not aware of anything in Haskell that can automatically derive an S-expression parser + pretty-printer.)

Proposal: evaluate aeson to (de)serialise FQ and SMT2 files.

Edit: alternatively / additionally, evaluate the sexp package to (de)serialise FQ and SMT2 files.

curiousleo commented 2 years ago

As it happens there is a fifth one: Horn.Parse :-)

Is this one different from what I called "SMT2 files", parsed by Horn.Parse.hornP? (I edited that comment several times -- if you receive GitHub comments via email, you may not have seen the most up to date version of that comment).

facundominguez commented 2 years ago

Perhaps it is a good time to mention that we have two kinds of file with .smt2 extension. One such kind is used for the horn format, and the other contains the logging of the smtlib2 text sent to the smt solver (and dumped in the .liquid directories).

Regarding FQ files, and the horn format, I don't think we can call them internal. They are the user facing format when liquid-fixpoint is used as a standalone executable, and probably there is some value in optimizing the format to make it the easiest to read for humans. But I rather defer to @nikivazou and @ranjitjhala on this matter.

ranjitjhala commented 2 years ago

Yes, that is correct -- thanks for the clarification!

On Thu, Nov 18, 2021 at 10:35 AM Facundo Domínguez @.***> wrote:

Perhaps it is a good time to mention that we have two kinds of file with .smt2 extension. One such kind is used for the horn format, and the other contains the logging of the smtlib2 text sent to the smt solver (and dumped in the .liquid directories).

Regarding FQ files, and the horn format, I don't think we can call them internal. They are the user facing format when liquid-fixpoint is used as a standalone executable, and probably there is some value in optimizing the format to make it the easiest to read for humans. But I rather defer to @nikivazou https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_nikivazou&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=NqpNcnkLj5Qa4pLRG5OCSk9qOjevHd-XfSlGpV54nG1ik2MgQPz_VBjkLxQUqFQW&s=OHLibIdUGvHYvXoklXyRCKno3TRxOgZhgCH4KJzXKa8&e= and @ranjitjhala https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ranjitjhala&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=NqpNcnkLj5Qa4pLRG5OCSk9qOjevHd-XfSlGpV54nG1ik2MgQPz_VBjkLxQUqFQW&s=OrYiBV2eBcRvH7Gs7ziCDFeu29CtOTwvplX88_8CnjA&e= on this matter.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_46-23issuecomment-2D973147392&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=NqpNcnkLj5Qa4pLRG5OCSk9qOjevHd-XfSlGpV54nG1ik2MgQPz_VBjkLxQUqFQW&s=j1hfry3SKp_hm4OFMotzuU40Q94Qek3JvrQZfW_0XNs&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OF5QMVVCRLKTSCSQITUMVBOBANCNFSM4A3VWEMQ&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=NqpNcnkLj5Qa4pLRG5OCSk9qOjevHd-XfSlGpV54nG1ik2MgQPz_VBjkLxQUqFQW&s=KMU4yTZRlThOBI1hkw-vVaAq-f9f3PTPVBKTgkQ1kYM&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=NqpNcnkLj5Qa4pLRG5OCSk9qOjevHd-XfSlGpV54nG1ik2MgQPz_VBjkLxQUqFQW&s=iTcvH_XtIla3dDewx8dPwPK1yJiy1rcJDeQs7meabIs&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=NqpNcnkLj5Qa4pLRG5OCSk9qOjevHd-XfSlGpV54nG1ik2MgQPz_VBjkLxQUqFQW&s=itearfqTQvskI2W0hio1eoi3kJvD0z9JsgIQtuMCaGs&e=.