hax icon indicating copy to clipboard operation
hax copied to clipboard
verified publisher icon hacspec

fix(engine/importer): use correct field to import concrete implexprs

Open paulmure opened this issue 1 year ago • 1 comments

Close #834.

@W95Psp some of the existing insta tests are failing and I'm not knowledgeable enough about them to see if they need to be updated.

paulmure avatar Aug 09 '24 00:08 paulmure

Hi, thanks for your PR! Sorry for the delay, the week is quite busy... will try to look into those tests tomorrow!

W95Psp avatar Aug 13 '24 15:08 W95Psp

Ok, I'm in a rush and so I rushed the review as well... I wanted to merge too fast, and actually I think there is a problem with the PR. Let me comment on the issue.

W95Psp avatar Sep 02 '24 07:09 W95Psp

@W95Psp As discussed in the issue, I'm trying to import the trait goal alongside the information stored in ImplExprAtom.

However, this seems to break the uses of ppx_inline in many of the modules in lib/phases. I guess it's caused by incorrect inlining of the code in subtype.ml. And I'm not sure how to fix this.

Any suggestions would be greatly appreciated!

paulmure avatar Sep 02 '24 18:09 paulmure

@W95Psp As discussed in the issue, I'm trying to import the trait goal alongside the information stored in ImplExprAtom.

However, this seems to break the uses of ppx_inline in many of the modules in lib/phases. I guess it's caused by incorrect inlining of the code in subtype.ml. And I'm not sure how to fix this.

Any suggestions would be greatly appreciated!

Forget what I said here, I think I just needed to run dune clean before building.

paulmure avatar Sep 03 '24 18:09 paulmure

After some back and forth, I decided to only import the trait goal for the concrete case for now. This avoids storing redundant copies of this trait goal since we are not using the ImplExprAtom pattern as in the exporter.

I'm not sure if it's actually needed for the other cases. If such a need arises in the future, we can reconsider how to import this information again.

All tests pass now. The only change is that the traits test for f* added a line of implicit dependency.

paulmure avatar Sep 03 '24 18:09 paulmure

Hi @paulmure, I'm reviewing this PR this morning, and I think I did something similar recently... https://github.com/hacspec/hax/pull/827 Sorry for the duplicate work... (the last month has been pretty work intensive toward a verification project...)

Wdyt, shall we close this one or is it still needed?

W95Psp avatar Oct 07 '24 06:10 W95Psp

That looks like the information we need. Thank you!

paulmure avatar Oct 10 '24 17:10 paulmure