Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Consolidate the output of the various dumps #546

Open
facundominguez opened this issue Apr 8, 2022 · 0 comments
Open

Consolidate the output of the various dumps #546

facundominguez opened this issue Apr 8, 2022 · 0 comments

Comments

@facundominguez
Copy link
Collaborator

facundominguez commented Apr 8, 2022

We have a few dumps from different parts of liquid-fixpoint. There is

.liquid/<input>.fq
.liquid/<input>.fq.pretiffied
.liquid/<input>.fq.ple
.liquid/<input>.fq.out

.fq and .fq.prettified show the initial input to LF. They contain liquid variables, and they are missing the equations discovered by ple and REST which are in (.fq.ple), and they miss the values assigned to liquid variables, which are present in .fq.out.

Navigating these files is possible, but probably it could be made simpler. I can imagine the following ways:

  1. Use hypertext to jump to definition sites (of bindings, equations, matches, liquid variables, lists of PLE equalities for a particular constraint, etc) and back.
  2. Consolidate all the information related to a constraint in one file. We would end up having one file per constraint, which might produce many files on some modules.

We could try to argue that we can just keep on with the files we have, since users aren't supposed to debug LH. However, once PLE or REST don't prove some constraint, the user will want to know what hypothesis are missing to prove it. And similarly, when working with abstract predicates, the user will want to know how the predicates are being inferred (maybe LH already can show this somehow?).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant