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

Agda decision tracing #6957

Merged
merged 32 commits into from
Mar 25, 2025
Merged
Changes from 1 commit
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
5f88cb9
WIP
ramsay-t Nov 5, 2024
d3cf588
WIP
ramsay-t Dec 3, 2024
8f3cddd
Merge branch 'master' into ramsay-t/semantic-equiv
ramsay-t Dec 3, 2024
028f627
WIP
ramsay-t Jan 27, 2025
41f9fb2
WIP - After meeting with Phil 28/01/25
ramsay-t Jan 28, 2025
d4f9876
WIP
ramsay-t Jan 21, 2025
c7b53c4
WIP
ramsay-t Feb 19, 2025
04726a1
Untested but typechecking WIP
ramsay-t Mar 7, 2025
025e53a
Merge Master
ramsay-t Mar 8, 2025
eb7d69c
Merge branch 'master' into ramsay-t/agda-decision-tracing
ramsay-t Mar 10, 2025
61e0204
WIP - pcePointwise working; lots of decision procedures left to update
ramsay-t Mar 12, 2025
df9bcae
WIP
ramsay-t Mar 12, 2025
9a087e3
WIP
ramsay-t Mar 12, 2025
8b4a25f
WIP
ramsay-t Mar 12, 2025
fe3e996
WIP - not working, Trace decisions need sorting.
ramsay-t Mar 12, 2025
a7d56e3
Typechecks...
ramsay-t Mar 13, 2025
6478d50
Add Certificate module to Agda build
ramsay-t Mar 13, 2025
0de4bf1
CE with tags.
ramsay-t Mar 17, 2025
f94301f
Resolved merge conflict but Ana's changes need to be added.
ramsay-t Mar 17, 2025
338cb9a
Re-enabled the 'dead' decision procedures
ramsay-t Mar 17, 2025
ee1155f
Added changelog
ramsay-t Mar 17, 2025
a5b92d0
Fixed a bug in the Translation module
ramsay-t Mar 17, 2025
091ac42
This test still fails
ramsay-t Mar 17, 2025
95c6580
Delete plutus-metatheory/src/Untyped/Reduction.lagda.md
ramsay-t Mar 17, 2025
7df3b09
Delete plutus-metatheory/src/Untyped/ContextualEquivalence.lagda.md
ramsay-t Mar 17, 2025
da53365
Cleanup PR
ramsay-t Mar 19, 2025
1882986
Returned the negative proofs
ramsay-t Mar 19, 2025
edbb14f
renamed function pceToDec
ramsay-t Mar 19, 2025
23944ba
Added FIXME note to Inline
ramsay-t Mar 19, 2025
7873698
Merge branch 'master' into ramsay-t/agda-decision-tracing
ramsay-t Mar 25, 2025
c4a827b
Some Agda printing/parsing fixes
ramsay-t Mar 25, 2025
cf564a9
Undo cabal change
ramsay-t Mar 25, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
This test still fails
ramsay-t committed Mar 17, 2025

Verified

This commit was signed with the committer’s verified signature.
ramsay-t Ramsay Taylor
commit 091ac42934a481bdff2f19a34fb094571165f422
2 changes: 1 addition & 1 deletion plutus-executables/test/certifier/Spec.hs
Original file line number Diff line number Diff line change
@@ -80,7 +80,7 @@ srcTests =
[ "inc"
-- TODO: This is currently failing to certify. This will be fixed
-- after the PR that covers counter example tracing.
-- , len
-- , "len"
]

makeExampleTests :: [ String ] -> [ TestTree ]