Unambig

[stschaef]

No description provided.

[maxsnew]

Is this ready? It's not building

[stschaef]

It should be ready. It's passing locally and I have no diffs from the remote.

I think I may have accidentally re-run old workflows (on older commits) instead of on the head. Running again now to be sure

[maxsnew]

It's showing some error to do with opaque:

/home/runner/work/grammars-and-semantic-actions/grammars-and-semantic-actions/code/cubical/NFA/Regex/Combinators.agda:218,15-18
warning: -W[no]UnfoldTransparentName
The name _⊕_, mentioned by an unfolding clause, does not belong to
an opaque block. This has no effect.
when scope checking the declaration
  import NFA.Regex.Combinators as .#NFA.Regex.Combinators-13138820953506565994
make: *** [Makefile:16: quicktest] Error 1

[maxsnew]

Also, please give more descriptive names and a short description to your PRs. This PR also makes a huge change which is to make stuff opaque which I only noticed because of the CI failure

[stschaef]

It's showing some error to do with opaque:

/home/runner/work/grammars-and-semantic-actions/grammars-and-semantic-actions/code/cubical/NFA/Regex/Combinators.agda:218,15-18
warning: -W[no]UnfoldTransparentName
The name _⊕_, mentioned by an unfolding clause, does not belong to
an opaque block. This has no effect.
when scope checking the declaration
  import NFA.Regex.Combinators as .#NFA.Regex.Combinators-13138820953506565994
make: *** [Makefile:16: quicktest] Error 1

This error makes no sense though, as this definition is opaque.

What I meant was that the CI ran on a commit before sum was made opaque, and I made the mistake of re-running that job rather than spawning a new one on the new commit. So I believe that the current commit will build and I'd been running the wrong job

[maxsnew]

Ok it's not erroring locally for me either so I'll merge