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 generics for proof serialising #6425

Closed
wants to merge 58 commits into from
Closed

Use Agda generics for proof serialising #6425

wants to merge 58 commits into from

Conversation

ana-pantilie
Copy link
Contributor

@ana-pantilie ana-pantilie commented Aug 20, 2024 •
edited
Loading

Needs #6413

Fixes #6424

  • updates the Agda standard-library to 2.0
  • updates agda to 2.6.4.3

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

kwxm and others added 30 commits August 13, 2024 09:19
@kwxm
WIP
dfde178
@kwxm
Merge branch 'master' into kwxm/metatheory/fix-test2
afa23a1
@kwxm
Fix broken metatheory tests using textual comparison
21607ed
@kwxm
Refactor detailed tests
f18ebe7
@kwxm
Refactor detailed tests
32c5a26
@kwxm
Re-enable plutus-metatheory:test2 in CI
9f17fba
@ana-pantilie
Add raw certification component
4d32e29 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@kwxm
Merge branch 'master' into kwxm/metatheory/fix-test2
540b95b
@kwxm
Fixes in project.nix
225ac43
@kwxm
Remove unused files
aa67c66
@zeme-wana
Remove the preCheck hack from plutus-metatheory.components.tests.test…
16d004c 
…-simple
@kwxm
Extra comments
68652b3
@kwxm
Merge branch 'kwxm/metatheory/fix-test2' of github.com:IntersectMBO/p…
5411479 
…lutus into kwxm/metatheory/fix-test2
@kwxm @zeme-wana
WIP
b3d582b
@kwxm @zeme-wana
Fix broken metatheory tests using textual comparison
a2dfbcd
@kwxm @zeme-wana
Refactor detailed tests
602d274
@kwxm @zeme-wana
Refactor detailed tests
48543fd
@kwxm @zeme-wana
Re-enable plutus-metatheory:test2 in CI
2f43b7b
@kwxm @zeme-wana
Fixes in project.nix
526e3eb
@kwxm @zeme-wana
Remove unused files
5d177dc
@kwxm @zeme-wana
Extra comments
8fe533f
@zeme-wana
Remove the preCheck hack from plutus-metatheory.components.tests.test…
948bc91 
…-simple
@zeme-wana
Rebase and remove dead code
fda7740
@ana-pantilie
WIP: fix compilation errors
3568d60 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@kwxm
Remove newline in error message
89f9b08
@kwxm
Merge branch 'kwxm/metatheory/fix-test2' of github.com:IntersectMBO/p…
35ee520 
…lutus into kwxm/metatheory/fix-test2
@ana-pantilie
Fix compilation errors
bcb1607 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Small clean-up
a2445ad 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@kwxm
Address some PR comments
e5ddb90
@kwxm
WIP
3d9c46a
kwxm and others added 25 commits August 16, 2024 09:57
@kwxm
Tidy up output of evaluation/typecheching results
36f8947
@kwxm
Tidy up output of evaluation/typecheching results
8c51c63
@kwxm
Name change
f9d5e2f
@ana-pantilie
WIP: clean-up
7ff26ec 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Merge remote-tracking branch 'origin/kwxm/metatheory/fix-test2' into …
f52e423 
…ana/add-certification-component
@ana-pantilie
Added plutus-executables package; moved uplc/pc/pir and metatheory tests
7778a19 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Add certifier to uplc optimiser
33b6482 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Add certifier to uplc optimise
1873aa8 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Merge remote-tracking branch 'origin/master' into ana/add-certificati…
99bd8ba 
…on-component
@ana-pantilie
Fix
8d8d0a2 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Clean-up
5733c83 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Clean-up cabal file
f451581 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Fix metatheory tests
6c70e1c 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Fix isTransformation?
c24e54e 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Certifier properly handles results
d06b49b 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Add documentation
9e42982 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Add a nix derivation for generics; upgrade stdlib to 2.1
d8fa57a 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Use standard-library 2.0; fix build
d1bb967
@ana-pantilie
Build MAlonzo with new stdlib
f0b9a85 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
WIP derive Show for Dec Trace
b7ce4fa
@ana-pantilie
Temp
dc339e3 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
WIP: add agda-stdlib-meta derivation
222190a 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Fix derivations
cc735cb 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Amazing
be317f6 
Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
@ana-pantilie
Merge remote-tracking branch 'origin/master' into ana/use-generics-in…
22a40f9 
…-metatheory
@ana-pantilie
Copy link
Contributor Author

Closed in favour of #6562

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Find a way to serialise Agda proof terms
3 participants
@ana-pantilie @kwxm @zeme-wana