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.

Sign up for GitHub

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

Jump to bottom

Use Agda Haskell lib instead of MAlonzo #6562

Open
wants to merge 32 commits into
base: master
Choose a base branch
from
Open

Use Agda Haskell lib instead of MAlonzo #6562

wants to merge 32 commits into from

Conversation

ana-pantilie
Copy link
Contributor

@ana-pantilie ana-pantilie commented Oct 11, 2024 •
edited
Loading

Fixes #6424

To test, do cabal exec uplc -- example -s factorial | cabal exec uplc -- optimise --certify factorialCert.

Pre-submit checklist:

  • Branch
    • Tests are provided (if possible)
    • Commit sequence broadly makes sense
    • Key commits have useful messages
    • Changelog fragments have been written (if appropriate)
    • Relevant tickets are mentioned in commit messages
    • Formatting, PNG optimization, etc. are updated
  • PR
    • (For external contributions) Corresponding issue exists and is linked in the description
    • Targeting master unless this is a cherry-pick backport
    • Self-reviewed the diff
    • Useful pull request description
    • Reviewer requested

@ana-pantilie ana-pantilie added the No Changelog Required Add this to skip the Changelog Check label Oct 29, 2024
@ana-pantilie ana-pantilie marked this pull request as ready for review October 29, 2024 12:46
@ana-pantilie ana-pantilie requested review from ramsay-t and a team October 29, 2024 12:47
@ana-pantilie ana-pantilie mentioned this pull request Oct 29, 2024
Closed
11 tasks
zliu41
zliu41 reviewed Oct 29, 2024
View reviewed changes
Copy link
Member

@zliu41 zliu41 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks quite reasonable. The example command took ~15s on my machine - is it mostly the decision procedure?

plutus-executables/executables/uplc/Main.hs
-- ^ The trace produced by the simplification process
-> IO ()
runCertifier (Just certName) (SimplifierTrace simplTrace) = do
let processAgdaAST Simplification {beforeAST, stage, afterAST} =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: add type signature so it is easier to tell what it does.

plutus-executables/src/AgdaUnparse.hs
instance AgdaUnparse AgdaFFI.UTerm where
agdaUnparse =
\case
AgdaFFI.UVar n -> "(UVar " ++ agdaUnparse (fromInteger n :: Natural) ++ ")"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps future work, but you can use pretty printing operators like <+> so that you don't need to worry about space.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, with pretty-printing we could have proper indentation for example. But I agree it's not too important.

@ana-pantilie
Copy link
Contributor Author

This seems to include all of the changes from #6512 that I merged yesterday. I'm not sure how that happened since that one had no overlap with this one.

Must have been a botched merge/rebase. I just rebased with master and I think it's fixed now. Thanks for noticing.

ramsay-t
ramsay-t approved these changes Oct 31, 2024
View reviewed changes
Copy link
Contributor

@ramsay-t ramsay-t left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good - it works nicely! I was going to delve into why it is slower than the other version, but I suspect that is because is actually serialising things, and not just printing "not implemented" :) I can come up with dozens of nice things we can do next, but those can wait for the next PR.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ramsay-t ramsay-t ramsay-t approved these changes

@zliu41 zliu41 zliu41 approved these changes

@effectfully effectfully effectfully approved these changes

Assignees
No one assigned
Labels
No Changelog Required Add this to skip the Changelog Check
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Find a way to serialise Agda proof terms
6 participants
@ana-pantilie @kwxm @ramsay-t @zliu41 @effectfully @zeme-wana