Ramsay t/translation efficiency 2 #6746

ramsay-t · 2024-12-12T15:09:17Z

I broke the other PR :( sorry. This one should be properly signed and mergable?

…suggestion that fixes the line explosion

…n-efficiency-2

ana-pantilie

@ramsay-t let me know when this is ready for review again.

ramsay-t · 2025-02-22T08:10:23Z

@ana-pantilie @Unisay I've done some fairly horrible things with our golden testing functions but it seems to work :) There are two examples - one currently certifying and one not - with a simple process to add more.

Yes, technically a test of the certifier ought to not invoke the optimiser and should use the AST stacks as input, rather than UPLC and calling the optimiser, but that would be really annoying to serialise and store. I would argue that if we change the optimiser enough to change the code it produces then we probably should re-read the certifier tests at least quickly to make we haven't changed anything the certifier should care about.

ana-pantilie · 2025-02-24T08:52:01Z

plutus-executables/changelog.d/20250222_080216_ramsay.taylor_translation_efficiency_2.rst

+Added
+-----
+
+- CI Tests for the certifier, using some simple unoptimised UPLC
+
+Changed
+-------
+
+- Complete reordering of decisions in UntypedTranslation.lagda.md


Usually we add user-facing changes to the changelog, so I'd remove these two.

ana-pantilie · 2025-02-24T08:59:18Z

plutus-metatheory/src/VerifiedCompilation/UntypedTranslation.lagda.md

-data Translation (R : Relation) { X : Set } {{_ : DecEq X}} : (X ⊢) → (X ⊢) → Set₁ where
-  istranslation : {ast ast' : X ⊢} → R ast ast' → Translation R ast ast'
-  var : {x : X} → Translation R (` x) (` x) -- We assume we won't want to translate variables individually?
+data Translation (R : Relation) { X : Set } {{_ : DecEq X}} : (X ⊢) → (X ⊢) → Set₁


Why does this have no constructors now?

It does, they've just moved to line 68 because it is co-inductive with the TransMatch definition, so the type signature has to be up here.

ana-pantilie · 2025-02-24T09:11:23Z

plutus-executables/test/certifier/Spec.hs

+    [ testGroup "simple certification"  $ makeTestTree simpleTests
+    , testGroup "failing certification"  $ makeTestTree failingTests


It's good that we can run tests on CI now, but an important aspect of testing is communicating intent: why do we expect the len test to fail?

As the comment above the definition on line 48 says: they "fail" in the sense that the certifier says "no" (currently). We will need to look into why that is, but you explicitly asked me to include this so we know the semantics aren't changed (until we do change them).

Usually you want to add tests which actually behave the way you expect them to. So this failing test should be transformed into a succeeding test, and commented out until it's fixed.

Perhaps "failing" is the wrong name - we want some tests that don't certify. Otherwise we are just demonstrating that the certifier says "yes", and not that it actually checks things. I'm not sure what English word you would prefer to "failing" in that case? Rejected, or Negative?

Yes, I know really we should have tests that we intend to be rejected, but I was hoping to avoid turning this into a solid week of test engineering ;) I shall do that though...

Unisay · 2025-02-24T14:56:30Z

Please re-format the plutus-executables/test/certifier/Spec.hs with fourmolu

Unisay · 2025-02-24T15:06:07Z

plutus-executables/test/certifier/Spec.hs

@@ -0,0 +1,62 @@
+{-# LANGUAGE OverloadedStrings #-}


This pragma is likely not needed as the language extension is already switched on by default in the cabal file.

Unisay · 2025-02-24T15:06:52Z

plutus-executables/test/certifier/Spec.hs

@@ -0,0 +1,62 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+{- | The tests in this file run tests of the uplc certifier. Various unoptimised UPLC is


Please lets keep lines within the 100 character width.

...this is 89?

I'm all for the classic 80 character limit if you'd prefer, but then lets set the github commit hook to enforce that.

ana-pantilie · 2025-02-24T15:10:27Z

Can you add the rest of the tests we were using to check the certifier manually? Like the ones generated by the uplc executable (factorial, fibonacci etc.).

effectfully

Fine by me, but to repeat my previous point I currently do not believe this is the right solution long-term despite it making things faster short-term. More on that here.

ramsay-t · 2025-02-25T09:26:19Z

Can you add the rest of the tests we were using to check the certifier manually? Like the ones generated by the uplc executable (factorial, fibonacci etc.).

The problem is they are randomly generated, so we can't do them as "golden" tests. Then we would have to decide what we are testing? Do we assume they all certify? Are we defining that as the last line of the response being "The compilation was successfully certified." - or do we actually set the exit code properly in the executable when certification fails?

ana-pantilie · 2025-02-25T10:28:56Z

@ramsay-t

The problem is they are randomly generated, so we can't do them as "golden" tests.

How are they randomly generated? They're just UPLC programs, we can add the UPLC code as you have with the other tests you added here.

Then we would have to decide what we are testing? Do we assume they all certify?

It doesn't make sense to have certifier integration tests which are expected to fail. That would mean that either the compiler or the certifier is broken in some way.

Are we defining that as the last line of the response being "The compilation was successfully certified." - or do we actually set the exit code properly in the executable when certification fails?

I think just checking the text is fine for now, we can improve that in the future.

ramsay-t · 2025-02-25T19:18:49Z

plutus-executables/plutus-executables.cabal

@effectfully this appears to have changed nothing in the CI :( perhaps you meant something different?

I think you need to import it, like it's done in this file with os-support.

Well, that fails fast at least :)

…C 8.10 because they depend on the Agda.

ana-pantilie · 2025-02-26T17:44:00Z

plutus-executables/test/certifier/Spec.hs

+-- These run but the certifier says "no"
+rejectedTests :: [String]
+rejectedTests =
+  [
+
+  ]


It doesn't make sense to keep this. It's dead code.

No it isn't its called on line 104 😸

ana-pantilie · 2025-02-26T17:44:18Z

plutus-executables/test/certifier/Spec.hs

+srcTests :: [ String ]
+srcTests =
+  [ "inc"
+  -- , len


At least add a comment describing why this test is not enabled.

ana-pantilie · 2025-02-26T17:47:34Z

plutus-executables/test/certifier/Spec.hs

+
+srcTests :: [ String ]
+srcTests =
+  [ "inc"


Can you please add the other tests as well as I asked? That should be very quick. I would normally be ok with you adding these in a separate PR, but since you decided to combine the testing framework with changes to the decision procedures as well, I will have to insist that you show that the changes to the decision procedures do not break any of the tests we have been running manually until now.

They are in the makeExample list....? Since they are generated from the executable it made more sense to let it generate fresh versions each time and certify those. We could include hardcoded instances or each of them, but the fresh ones are maybe more interesting?

I missed that, sorry. Thanks for making the changes!

Except: why do these never trigger the bug that the short “len” example triggers? They are probably already optimised and so are just returning an ID change all the time…. If we can make them unoptimised then they will be more useful but will currently fail (possibly randomly?)

I remember that the uplc examples are unoptimised. If I printed the factorial or whatever script, I remember seeing force ... delays that could definitely be reduced.

Looking at the generated certificates, there does seem to be some changes happening, so these are meaningful tests - although they might be more meaningful if we used the plc examples and then fed those in so there was more work happening...

I think we were typing at the same time :) These are fine for now, although I could spend ages improving them!

ramsay-t added 4 commits November 27, 2024 13:42

Translation now tries match first and then R. Includes Ulf Norrell's …

4b0b0e9

…suggestion that fixes the line explosion

Fixed examples that use Translation

34172ef

merge

a7715fe

Merge remote-tracking branch 'origin/master' into HEAD

5290592

ramsay-t added Metatheory No Changelog Required Add this to skip the Changelog Check labels Dec 12, 2024

ramsay-t self-assigned this Dec 12, 2024

ramsay-t temporarily deployed to github-pages December 12, 2024 15:09 — with GitHub Actions Inactive

ramsay-t requested review from effectfully and ana-pantilie December 12, 2024 15:09

Merge remote-tracking branch 'origin/master' into ramsay-t/translatio…

c90a74c

…n-efficiency-2

ana-pantilie temporarily deployed to github-pages February 6, 2025 13:48 — with GitHub Actions Inactive

Fix to Agda rendering of constr

9b8cd7d

ramsay-t temporarily deployed to github-pages February 13, 2025 11:46 — with GitHub Actions Inactive

Merge branch 'master' into ramsay-t/translation-efficiency-2

ad0d503

ramsay-t temporarily deployed to github-pages February 13, 2025 11:49 — with GitHub Actions Inactive

ana-pantilie reviewed Feb 14, 2025

View reviewed changes

Merge branch 'master' into ramsay-t/translation-efficiency-2

617b0a8

ramsay-t temporarily deployed to github-pages February 18, 2025 07:05 — with GitHub Actions Inactive

WIP - CI

2c37cc5

ramsay-t temporarily deployed to github-pages February 21, 2025 16:18 — with GitHub Actions Inactive

WIP - CI

277e03f

ramsay-t temporarily deployed to github-pages February 21, 2025 16:33 — with GitHub Actions Inactive

Now with a couple of CI examples

c80fa82

ramsay-t temporarily deployed to github-pages February 22, 2025 07:57 — with GitHub Actions Inactive

ramsay-t removed the No Changelog Required Add this to skip the Changelog Check label Feb 22, 2025

Changelog

b7d937f

ramsay-t temporarily deployed to github-pages February 22, 2025 08:04 — with GitHub Actions Inactive

Merge branch 'master' into ramsay-t/translation-efficiency-2

6926faa

ana-pantilie reviewed Feb 24, 2025

View reviewed changes

ramsay-t requested a review from Unisay February 24, 2025 09:29

Unisay reviewed Feb 24, 2025

View reviewed changes

effectfully approved these changes Feb 24, 2025

View reviewed changes

WIP - more CI, better CI

7d61514

ramsay-t temporarily deployed to github-pages February 25, 2025 10:26 — with GitHub Actions Inactive

ramsay-t added 2 commits February 25, 2025 15:08

Changelog

cdee428

Merge branch 'master' into ramsay-t/translation-efficiency-2

4535a0b

ramsay-t temporarily deployed to github-pages February 25, 2025 15:09 — with GitHub Actions Inactive

Disable GHC 8.10 for metatheory and executables

0fbf687

ramsay-t temporarily deployed to github-pages February 25, 2025 15:34 — with GitHub Actions Inactive

ramsay-t commented Feb 25, 2025

View reviewed changes

Disable GHC 8.10 for metatheory and executables...properly

37820ab

ramsay-t temporarily deployed to github-pages February 26, 2025 06:42 — with GitHub Actions Inactive

Made some benchmark and conformance components not compatible with GH…

7f5c747

…C 8.10 because they depend on the Agda.

ramsay-t temporarily deployed to github-pages February 26, 2025 12:11 — with GitHub Actions Inactive

ana-pantilie requested changes Feb 26, 2025

View reviewed changes

Removed currently unused rejected tests.

740c473

ramsay-t temporarily deployed to github-pages February 26, 2025 18:58 — with GitHub Actions Inactive

ana-pantilie approved these changes Feb 26, 2025

View reviewed changes

ramsay-t requested a review from Unisay February 27, 2025 12:16

Merge branch 'master' into ramsay-t/translation-efficiency-2

c36ce9f

ramsay-t temporarily deployed to github-pages March 4, 2025 09:06 — with GitHub Actions Inactive

ramsay-t merged commit 87c89d6 into master Mar 4, 2025
8 checks passed

ramsay-t deleted the ramsay-t/translation-efficiency-2 branch March 4, 2025 11:24

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Ramsay t/translation efficiency 2 #6746

Ramsay t/translation efficiency 2 #6746

ramsay-t commented Dec 12, 2024

ana-pantilie left a comment

ramsay-t commented Feb 22, 2025

ana-pantilie Feb 24, 2025

ana-pantilie Feb 24, 2025

ramsay-t Feb 24, 2025

ana-pantilie Feb 24, 2025

ramsay-t Feb 24, 2025

ana-pantilie Feb 24, 2025

ramsay-t Feb 25, 2025

ramsay-t Feb 25, 2025

Unisay commented Feb 24, 2025

Unisay Feb 24, 2025

Unisay Feb 24, 2025

ramsay-t Feb 25, 2025

ana-pantilie commented Feb 24, 2025

effectfully left a comment

ramsay-t commented Feb 25, 2025

ana-pantilie commented Feb 25, 2025 •

edited

Loading

ramsay-t Feb 25, 2025

effectfully Feb 25, 2025

ramsay-t Feb 26, 2025

ana-pantilie Feb 26, 2025

ramsay-t Feb 26, 2025

ana-pantilie Feb 26, 2025

ana-pantilie Feb 26, 2025

ramsay-t Feb 26, 2025

ana-pantilie Feb 26, 2025

ramsay-t Feb 27, 2025

ana-pantilie Feb 27, 2025

ramsay-t Feb 27, 2025

ramsay-t Feb 27, 2025

		[ testGroup "simple certification" $ makeTestTree simpleTests
		, testGroup "failing certification" $ makeTestTree failingTests

		@@ -0,0 +1,62 @@
		{-# LANGUAGE OverloadedStrings #-}

		{- \| The tests in this file run tests of the uplc certifier. Various unoptimised UPLC is

Ramsay t/translation efficiency 2 #6746

Ramsay t/translation efficiency 2 #6746

Conversation

ramsay-t commented Dec 12, 2024

ana-pantilie left a comment

Choose a reason for hiding this comment

ramsay-t commented Feb 22, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Unisay commented Feb 24, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ana-pantilie commented Feb 24, 2025

effectfully left a comment

Choose a reason for hiding this comment

ramsay-t commented Feb 25, 2025

ana-pantilie commented Feb 25, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ana-pantilie commented Feb 25, 2025 •

edited

Loading