[ test ] Fix spec001 test

[dunhamsteve]

Description

The spec001 test appears to be broken in CI because the numbers in the machine names are different in CI in the test output. This is noted in #3155. Inspired by 1aff26e, I'm rewriting the numbers in resolved, arg, and conArg machine names to be XXX in the test output.

[mattpolzin]

The only question in my mind is whether this test output was supposed to be useful in spotting a change that actually caused argument numbers to change not just from x to y but from x to sometimes y and sometimes z (i.e. inconsistently). I really don't know, maybe that's not at all a perceived benefit because it's so unlikely and/or would be caught by other tests if it occurred.

[dunhamsteve]

I took a closer look at why these numbers are different.

Where they are different, the args and conArgs are 138 higher and $resolved is 2 higher. For resolved, I think this can happen by two more names in the global context.

I bisected locally and it looks like f2e6dc4 introduced the change:

FAIL f2e6dc431 Add dependent congruence of arity 1 and 2 for heterogeneous equality [G. Allais]
PASS 82e4fd9da Add foldrImplGoLemma to Data.Vect (#2835) [GitHub]

The change adds two functions to the Prelude, which explains $resolved. And the args and conArgs changes look like they're machine generated names inside the prelude, e.g. (this is a git "word diff")

(Just [-{arg:8742})-]{+{arg:8880})+} a b)

I don't think we can avoid a bunch of these numbers changing any time we add something to the prelude. Dunno if there is a better solution, other than updating the tests whenever things change. At least the fact that specialization is happening, and the general shape of things are captured in the output.

[buzden]

whether this test output was supposed to be useful in spotting a change that actually caused argument numbers to change

I think since there is no specification on what values those numbers have to be and anyway are changed blindly in any change in prelude and/or imported libraries, it is definitely okay for now. As soon as the logic of numbering is changed to be more stable, is can be revised.

The only thing, I think, that can be improved is not just hiding those numbers but bijecively mapping them to new ones with a stable numbering (say, local to particular test) so that we can check in a test that equal machine names indeed stay equal in the output, and different ones indeed stay different. But, I think, this is not a thing that should be required for this PR.

[dunhamsteve]

A more complicated awk script might be able to assign new numbers as it finds them in the log (and maintain the mapping of scene stuff). Ideally the $resolved stuff would handled by use of toFullNames.

So now I've got one of those situations where I've thought through a solution and want to implement it.

[mattpolzin]

@dunhamsteve that's an impressive awk script! I hesitate to be the one to officially approve or merge this, but I'm quite happy with your solution for my part!

[gallais]

Inspired by 1aff26e, I'm rewriting the numbers in resolved, arg, and conArg machine names to be XXX in the test output.

Should we have a unique function in testutils implementing that cleanup strategy uniformly?

[buzden]

Should we have a unique function in testutils implementing that cleanup strategy uniformly?

I think we defintely should!

BTW, @dunhamsteve, can I take your code to use in the tests in my own projects, outside the compiler?

[dunhamsteve]

Feel free to use the script elsewhere.

In testutils, would this look like a clean_names function and the user still has to do:

{
...commands
} | clean_names

Or would it be a special version of the idris2 function that runs idris and applies the filtering?

[gallais]

I'd be in favour of clean_names, yes.

[dunhamsteve]

I've moved the function into testutils. It is clean_names and used as described above. I had to silence the linter on one line of code, because it was upset that I was hiding $ references from the shell.

[gallais]

Can we use it for the test cases in find tests/ -name "run" | xargs grep " sed "?

[dunhamsteve]

We can use it as-is for many of them, for the others, we’d have to add the [0-9]+:[0-9]+ regex. I guess that is for the FC printing? Probably okay to rewrite those too in all cases. I’ll try to find some time tonight for that.

[gallais]

I don't mind if the golden values change. Uniformity first and foremost.

[dunhamsteve]

Ok, I've added support for:

   ttc/NNNNNNNNNN
   Foo.Bar:NN:NN--NN:NN
   P:xyz:NNNNN

Which covers most of the other sed cases.

There was one case that was special for src/TTImp/ProcessDef.idr, because it printed a bare resolved number rather than the $resolved name. I decided to address that with (getFullName (Resolved n)) rather than (Resolved n). I figured the real name would be more useful to users.

[gallais]

Fantastic!

[buzden]

@dunhamsteve I finally used your script from this PR for tests of my library, and I found out that it renames values unexpectedly. For example, I have the following diff after that:

                (MkTy <DerivedGen.X>[0, 1, 2, 3]
                      (IPi.  (MW ExplicitArg : IVar Data.Fuel.Fuel)
-                         -> (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat)
-                         -> (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat)
-                         -> (MW ExplicitArg {arg:3636} : IVar Prelude.Types.Nat)
-                         -> (MW ExplicitArg {arg:3639} : IVar Prelude.Types.Nat)
+                         -> (MW ExplicitArg {arg:1} : IVar Prelude.Types.Nat)
+                         -> (MW ExplicitArg {arg:1} : IVar Prelude.Types.Nat)
+                         -> (MW ExplicitArg {arg:1} : IVar Prelude.Types.Nat)
+                         -> (MW ExplicitArg {arg:1} : IVar Prelude.Types.Nat)
                          -> (IApp. IVar Test.DepTyCheck.Gen.Gen
                                  $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty
                                  $ (IApp. IVar DerivedGen.X
-                                        $ IVar {arg:3630}
-                                        $ IVar {arg:3633}
-                                        $ IVar {arg:3636}
-                                        $ IVar {arg:3639}))))
+                                        $ IVar {arg:1}
+                                        $ IVar {arg:1}
+                                        $ IVar {arg:1}
+                                        $ IVar {arg:1}))))
         IDef <DerivedGen.X>[0, 1, 2, 3]
              [ PatClause (IApp. IVar <DerivedGen.X>[0, 1, 2, 3]

Am I right that your script should have renamed those variables to {arg:1}, {arg:2}, {arg:3} and {arg:4} respectively, not all of them to {arg:1}?

[dunhamsteve]

Yeah, that was my intent. That they would get unique names, but a consistent mapping for a given name if it recurs later in the input. I can take a look after work (PST).

[dunhamsteve]

"There are 2 hard problems in computer science: cache invalidation, naming things, and off-by-1 errors."

Couldn't resist taking a look now. It seems that it was ignoring the last digit of the name. (I printed m as part of the name to sort this out):

diff --git a/tests/testutils.sh b/tests/testutils.sh
index 04b588cb2..d96684324 100755
--- a/tests/testutils.sh
+++ b/tests/testutils.sh
@@ -57,7 +57,7 @@ _awk_clean_name='
     while (match($0, /(P:[A-z]+:|arg:|conArg:|ttc[\\\/][0-9]+|[$]resolved)[0-9]+|[A-z.]+:[0-9]+:[0-9]+--[0-9]+:[0-9]+|[A-z]+[.][0-9]+:[0-9]+/)) {
         rs = RSTART
         rl = RLENGTH
-        m = substr($0, rs, rl - 1)
+        m = substr($0, rs, rl)
         pfx = "XXX"
         if (match(m,/^(\$resolved|arg:|conArg:|ttc[\\\/]|P:[A-z]+:|[A-z.]+:|[A-z]+[.])/)) { pfx = substr(m, RSTART, RLENGTH) }
         if (!(m in mapping)) {

I had to update a couple of expected files after making this fix. I can PR after CI runs. Thanks for catching this.