Broken Interaction Tests [Re: [Agda] Re: Syntax for anonymous functions]

[Andreas Abel]

Hello Fredrik an Nisse,

for the interaction test, I get

Issue373.out Issue373.tmp differ: char 42, line 2
=== Old output ===
agda2_mode_code (agda2-status-action "")
[1 of 3] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
[2 of 3] Compiling Imports.Nat      ( Imports/Nat.hs, Imports/Nat.o )
[3 of 3] Compiling MAlonzo.Code.Issue373 ( MAlonzo/Code/Issue373.hs, 
MAlonzo/Code/Issue373.o )
agda2_mode_code (agda2-status-action "Checked")
agda2_mode_code (agda2-info-action
                  "*Compilation result*"
                  "The module was successfully compiled.")
agda2_mode_code (agda2-goals-action '())
ok
=== New output ===
agda2_mode_code (agda2-status-action "")
agda2_mode_code (agda2-status-action "Checked")
agda2_mode_code (agda2-info-action
                  "*Compilation result*"
                  "The module was successfully compiled.")
agda2_mode_code (agda2-goals-action '())
ok
=== Diff ===
2,4d1
< [1 of 3] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
< [2 of 3] Compiling Imports.Nat      ( Imports/Nat.hs, Imports/Nat.o )
< [3 of 3] Compiling MAlonzo.Code.Issue373 ( MAlonzo/Code/Issue373.hs, 
MAlonzo/Code/Issue373.o )
make[1]: *** [Issue373.cmp] Error 1
make: *** [interaction] Error 2

@Nisse: How do I repair this test case?

These interaction tests seem to degenerate.  They work on a freshly 
pulled Agda, but after some time I see them failing.

Which files do I need to delete or regenerate and how?

Cheers,
Andreas

P.S.: Maybe the Makefile could be changed to make this test case more 
robust, e.g., just compare the last 5 lines or so.

On 5/25/11 11:26 AM, Nils Anders Danielsson wrote:
> On 2011-05-24 21:52, Fredrik Nordvall Forsberg wrote:
>> This is a bit heavyweight for a small function, though, so we have also
>> introduced the syntax
>>
>> (a , b) |-> a
>>
>> for one clause functions. The Unicode-inclined can use \mapsto in the
>> emacs mode.
>
> Adding both function and ↦ as keywords seems excessive to me. Would the
> following syntax work?
>
> { p₁ ↦ e₁; p₂ ↦ e₂; … }
>
>> By the way, am I the only one for which test/interaction/Issue373.agda
>> doesn't output
>>
>> [1 of 3] Compiling MAlonzo.RTE ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
>> [2 of 3] Compiling Imports.Nat ( Imports/Nat.hs, Imports/Nat.o )
>> [3 of 3] Compiling MAlonzo.Code.Issue373 ( MAlonzo/Code/Issue373.hs,
>> MAlonzo/Code/Issue373.o )
>>
>> when running the test suite?
>
> I get the following output (in Issue373.out):
>
> agda2_mode_code (agda2-status-action "")
> [1 of 3] Compiling MAlonzo.RTE ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
> [2 of 3] Compiling Imports.Nat ( Imports/Nat.hs, Imports/Nat.o )
> [3 of 3] Compiling MAlonzo.Code.Issue373 ( MAlonzo/Code/Issue373.hs,
> MAlonzo/Code/Issue373.o )
> agda2_mode_code (agda2-status-action "Checked")
> agda2_mode_code (agda2-info-action
> "*Compilation result*"
> "The module was successfully compiled.")
> agda2_mode_code (agda2-goals-action '())
> ok
>
>> Or who gets the error message
>>
>> Not implemented: primQNameType
>>
>> when compiling std-lib/src/Reflection.agdai in the compiler tests?
>
> I think some people tend to skip the compiler test suite—it can take
> roughly an hour to run, so that is not very strange. We should use a
> quicker test (which also includes the Epic backend). Contributions are
> welcome.
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/