Andreas Abel

Observed again today: https://github.com/agda/agda/actions/runs/10683742640/job/29612530382?pr=7469#step:7:10 I wonder what the conditions for `cabal v2-install` are to skip building.

These two commits passed CI when based onto `master`. Now I rebased them onto `merge-v2.1.1` so I can use them with Agda master (2.8.0).

Unfortunately, CI does not run anymore since the merge base is not `master` anymore. I will have to change it back to master once #2473 has landed: - #2473

I reset `experimental` to current `master` and rebased this PR onto `experimental`. So we are back in the main stream now.

> As this is a breaking change, is it possible to wait until we know for sure that Agda will also make the breaking change? Yes, let's wait until the...

This PR was only addressing recursive records for which Agda cannot detect that they are guarded. The prime example for an unguarded record type would be this one: ```agda record...

> @andreasabel what is the status of this? Did this change make it into v2.8.0? No, it didn't, so I didn't merge this PR into `experimental`. So I guess it...

I think I got this one wrong. The combination of those flags just turns off termination checking completely, which Agda allows unless `--safe`.

Adding also `libgmp-static` indeed fixes the workflow. Big thanks!

@nad wrote: > The documentation could be more explicit about how whitespace is treated. For instance, what happens if the `executables` file contains the following text? > > ``` >...