Skip to content

Error "case_of_ must be fully applied to a lambda term in "Generate test-suite HTML" CI action #436

@jespercockx

Description

@jespercockx

Currently CI fails due to a strange error in test/Fail/PartialCase.agda:

Generating HTML for AllFailTests (html/AllFailTests.html).
/home/runner/work/agda2hs/agda2hs/test/Fail/PartialCase.agda:5.1-7: error: [CustomBackendError]
agda2hs: case_of_ must be fully applied to a lambda term
make[1]: *** [Makefile:54: html/AllFailTests.html] Error 42
make[1]: Leaving directory '/home/runner/work/agda2hs/agda2hs/test'
make: *** [Makefile:30: testHtml] Error 2
Error: Process completed with exit code 2.

Failing run: https://github.com/agda/agda2hs/actions/runs/18348868257/job/52262916249

I'm not sure what's going on here. Why are we generating HTML from the test suite in the first place? Why do we still try to generate Haskell code when generating HTML? Why did this ever work before?

Metadata

Metadata

Assignees

Labels

bugSomething isn't workinghelp wantedExtra attention is needed

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions