Andreas Abel

@nad wrote: > I constructed a small test case from the standard library code: > > ```agda > {-# OPTIONS --without-K #-} > > P : Set → Set₁ >...

For example (error message involving `with`) see - #5866

> Why not assigning numbered ids to every identifier, just like it is done with the identifier of the main module and the unnamed module? There are UIDs (numbers) for...

> are names taken away from html generation? I am using 2.6.2.1 and I see no identifier in the generated html. They should be there, e.g. `` in the following...

> in that case, wouldn't it make sense to not even wrap the `` with id around the code as well? What would be gained by that? I just added...

> Is there a simple and efficient way to figure out if a `QName` was declared as a public or a private name? Not sure. AFAIK, the scope machinery cares...

Weird. In workflow `cabal-test`, we are actually _installing_ Agda which means that the interface files for the builtin modules should be already there before the tests run: https://github.com/agda/agda/blob/bea11a04df5f82b2b8782bcad5bf2af2a6b88b65/src/github/workflows/cabal-test.yml#L101-L110 https://github.com/agda/agda/blob/bea11a04df5f82b2b8782bcad5bf2af2a6b88b65/Setup.hs#L38-L49 Unfortunately,...

The interface files are indeed created, see https://github.com/agda/agda/runs/4024146696?check_suite_focus=true: ``` ... /tmp/cabal-install.-15469/dist-newstyle/tmp/src-15469/Agda-2.6.3/src/data/lib/prim/Agda/Builtin/Sigma.agda ... Installing executable agda in /home/runner/.cabal/store/ghc-9.0.1/incoming/new-15469/home/runner/.cabal/store/ghc-9.0.1/Agda-2.6.3-23c03e2f454ccd070c046a54abbe9d4228ebf4453339a72faec00346d21fc8a0/bin ``` Questions: 1. Are the copied to the install location? 2. Are they...

This race condition now plagues also the `test.yml` workflow. https://github.com/agda/agda/runs/6919763105?check_suite_focus=true#step:9:29

@mergifyio rebase