`--build-library` handling of `--guardedness`

Open felixwellen opened this issue 6 months ago • 1 comments

Agda 2.8.0 seems to integrate all modules in one (virtual) module when using the --build-library-flag. This has the effect, that it is not possible to use, e.g. --guardedness just in some modules of the library, like it is currently done in cubical (e.g. v0.8). This showed when upgrading cubical to agda 2.8.0 in this PR: https://github.com/agda/cubical/pull/1222 where agda would fail without the --guardedness-flag in cubical.agda-lib with:

/home/runner/work/cubical/cubical/Cubical/Codata/Conat.agda:1.1: error: [InfectiveImport]
Importing module Cubical.Codata.Conat using the --guardedness flag
from a module which does not.

Jul 16 '25 12:07 felixwellen

--guardedness is an infective option, but those warnings should be filtered out: https://github.com/agda/agda/blob/822e0aee235ba787b7ac50cc7ab19fca20be5924/src/full/Agda/Interaction/BuildLibrary.hs#L95-L104 Not sure why this does not work in all situations yet.

Jul 16 '25 14:07 andreasabel