Import libraries from a system path

[kleinreact]

Import libraries from a system path

[kleinreact]

I've added two files (please remove the additional file ending, which just was required for direct upload here)

• Level.agdai-system.txt
  The interface file generated during the system installation.
• Level.agdai-rebuild.txt
  The interface file generated by the local user. To this end, I just copied all of /usr/share/agda-stdlib to a local folder and updated ~/.config/agda/libraries to point to that folder instead. Then everything works, as Agda has write permissions to update the interface files. This is the updated Level.agdai resulting from this.

@jamesmckinna Yeah, I noticed that when I updated the Gentoo ebuild to the latest 2.0 release for this issue report. However, I ran into the same issue with agda-stdlib 1.7.2 and Agda 1.6.3.0 before, which are the latest versions Gentoo currently offers via the Haskell Overlay.

[UlfNorell]

Do you have the command used to install the std-lib? The only thing I can think of is that it was installed with different options turned on, making the interface files incompatible.

It also would be ok to have a local copy of the interface files in some _build directory of the project folder being generated via checking the system files again once per project.
Unfortunately, I haven't found a command line option of agda for doing this either. Is this meant to be supported in any way?

This is not currently supported, but it might be worth filing an issue for it, since it's not an unreasonable thing to have.

[kleinreact]

The main command does

agda +RTS -K1G -RTS -i . -i src Everything.agda

after running the GenerateEverything script without any options. However, running

agda +RTS -K1G -RTS Test.agda --trace-imports=3 --compile-dir=.

runs into the same problem. So I cannot see any problem with the options. It may also be the sandbox compilation resulting in some wrong paths stored in the interface files.

[UlfNorell]

That shouldn't be the case. You can take a compiled project and move it to a different path without triggering recompilation.

Would you be willing to build Agda with debugging enabled? That would let us get more information about why it doesn't like the interface file.

It should be as simple as cabal install Agda -fdebug --program-suffix=-debug. You can then run

agda-debug Test.agda -v import:10 --compile-dir=.

to get more detailed information about what is happening.

[kleinreact]

I get the following with the debug flag enabled:

Importing the primitive modules.
  Getting interface for Agda.Primitive
  Check for cycle
  Agda.Primitive is up-to-date.
  no stored version, reading /home/user/.cabal/store/ghc-9.4.5/Agda-2.6.4.1-753a2d77d7fa58be8080e15e6af3140fb7fde76cd5aee74b85932a86128b2270/share/lib/prim/Agda/Primitive.agdai
Loading  Agda.Primitive (/home/user/.cabal/store/ghc-9.4.5/Agda-2.6.4.1-753a2d77d7fa58be8080e15e6af3140fb7fde76cd5aee74b85932a86128b2270/share/lib/prim/Agda/Primitive.agdai).
  imports: []
  New module. Let's check it out.
Merging interface
  Now we've looked at Agda.Primitive
  Getting interface for Agda.Primitive.Cubical
  Check for cycle
  Agda.Primitive.Cubical is up-to-date.
  no stored version, reading /home/user/.cabal/store/ghc-9.4.5/Agda-2.6.4.1-753a2d77d7fa58be8080e15e6af3140fb7fde76cd5aee74b85932a86128b2270/share/lib/prim/Agda/Primitive/Cubical.agdai
Loading  Agda.Primitive.Cubical (/home/user/.cabal/store/ghc-9.4.5/Agda-2.6.4.1-753a2d77d7fa58be8080e15e6af3140fb7fde76cd5aee74b85932a86128b2270/share/lib/prim/Agda/Primitive/Cubical.agdai).
  imports: [(Agda.Primitive, 450520314077838934)]
  Already visited Agda.Primitive
  New module. Let's check it out.
Merging interface
  Now we've looked at Agda.Primitive.Cubical
Done importing the primitive modules.
  Getting interface for Test
  Check for cycle
  Test is not up-to-date because the interface has not been decoded and the interface file could not be found.
Checking Test (/home/user/Test.agda).
Creating interface for Test.
  visited: Agda.Primitive, Agda.Primitive.Cubical
Starting scope checking.
Scope checking Agda.Primitive
  visited: Agda.Primitive, Agda.Primitive.Cubical
  Already visited Agda.Primitive
Scope checking Data.Nat
  visited: Agda.Primitive, Agda.Primitive.Cubical
  Getting interface for Data.Nat
  Check for cycle
  Data.Nat is up-to-date.
  no stored version, reading /usr/share/agda-stdlib/_build/2.6.4.1/agda/Data/Nat.agdai
 Loading  Data.Nat (/usr/share/agda-stdlib/_build/2.6.4.1/agda/Data/Nat.agdai).
  imports: [(Data.Nat.Properties, 8284414203852770123),
 (Agda.Primitive, 450520314077838934),
 (Data.Nat.Base, 39242842772408985)]
  Data.Nat is not up-to-date because the interface has not been decoded and options changed.
 Checking Data.Nat (/usr/share/agda-stdlib/Data/Nat.agda).
Creating interface for Data.Nat.
  visited: Agda.Primitive, Agda.Primitive.Cubical
Starting scope checking.
Scope checking Agda.Primitive
  visited: Agda.Primitive, Agda.Primitive.Cubical
  Already visited Agda.Primitive
Scope checking Data.Nat.Base
  visited: Agda.Primitive, Agda.Primitive.Cubical
  Getting interface for Data.Nat.Base
  Check for cycle
  Data.Nat.Base is up-to-date.
  no stored version, reading /usr/share/agda-stdlib/_build/2.6.4.1/agda/Data/Nat/Base.agdai
  Loading  Data.Nat.Base (/usr/share/agda-stdlib/_build/2.6.4.1/agda/Data/Nat/Base.agdai).
  imports: [(Relation.Unary, 7715865622099666514),
 (Relation.Binary.PropositionalEquality.Core, 10201387887212518222),
 (Algebra.Definitions.RawMagma, 4697865347224375591),
 (Data.Parity.Base, 10463527604420964418),
 (Agda.Primitive, 450520314077838934),
 (Data.Bool.Base, 13291421676770665970),
 (Agda.Builtin.Nat, 6430282414199393794),
 (Relation.Nullary.Negation.Core, 13274003286046970988),
 (Algebra.Bundles.Raw, 1733169355009022169),
 (Relation.Binary.Core, 7490461068912438315),
 (Level, 6767709025310621275)]
  Data.Nat.Base is not up-to-date because the interface has not been decoded and options changed.
  Checking Data.Nat.Base (/usr/share/agda-stdlib/Data/Nat/Base.agda).
Creating interface for Data.Nat.Base.
  visited: Agda.Primitive, Agda.Primitive.Cubical
Starting scope checking.
Scope checking Agda.Primitive
  visited: Agda.Primitive, Agda.Primitive.Cubical
  Already visited Agda.Primitive
Scope checking Algebra.Bundles.Raw
  visited: Agda.Primitive, Agda.Primitive.Cubical
  Getting interface for Algebra.Bundles.Raw
  Check for cycle
  Algebra.Bundles.Raw is up-to-date.
  no stored version, reading /usr/share/agda-stdlib/_build/2.6.4.1/agda/Algebra/Bundles/Raw.agdai
   Loading  Algebra.Bundles.Raw (/usr/share/agda-stdlib/_build/2.6.4.1/agda/Algebra/Bundles/Raw.agdai).
  imports: [(Agda.Primitive, 450520314077838934),
 (Algebra.Core, 1670221008836805456),
 (Relation.Nullary.Negation.Core, 13274003286046970988),
 (Relation.Binary.Core, 7490461068912438315),
 (Level, 6767709025310621275)]
  Algebra.Bundles.Raw is not up-to-date because the interface has not been decoded and options changed.
   Checking Algebra.Bundles.Raw (/usr/share/agda-stdlib/Algebra/Bundles/Raw.agda).
Creating interface for Algebra.Bundles.Raw.
  visited: Agda.Primitive, Agda.Primitive.Cubical
Starting scope checking.
Scope checking Agda.Primitive
  visited: Agda.Primitive, Agda.Primitive.Cubical
  Already visited Agda.Primitive
Scope checking Algebra.Core
  visited: Agda.Primitive, Agda.Primitive.Cubical
  Getting interface for Algebra.Core
  Check for cycle
  Algebra.Core is up-to-date.
  no stored version, reading /usr/share/agda-stdlib/_build/2.6.4.1/agda/Algebra/Core.agdai
    Loading  Algebra.Core (/usr/share/agda-stdlib/_build/2.6.4.1/agda/Algebra/Core.agdai).
  imports: [(Agda.Primitive, 450520314077838934),
 (Level, 6767709025310621275)]
  Algebra.Core is not up-to-date because the interface has not been decoded and options changed.
    Checking Algebra.Core (/usr/share/agda-stdlib/Algebra/Core.agda).
Creating interface for Algebra.Core.
  visited: Agda.Primitive, Agda.Primitive.Cubical
Starting scope checking.
Scope checking Agda.Primitive
  visited: Agda.Primitive, Agda.Primitive.Cubical
  Already visited Agda.Primitive
Scope checking Level
  visited: Agda.Primitive, Agda.Primitive.Cubical
  Getting interface for Level
  Check for cycle
  Level is up-to-date.
  no stored version, reading /usr/share/agda-stdlib/_build/2.6.4.1/agda/Level.agdai
     Loading  Level (/usr/share/agda-stdlib/_build/2.6.4.1/agda/Level.agdai).
  imports: [(Agda.Primitive, 450520314077838934)]
  Level is not up-to-date because the interface has not been decoded and options changed.
     Checking Level (/usr/share/agda-stdlib/Level.agda).
Creating interface for Level.
  visited: Agda.Primitive, Agda.Primitive.Cubical
Starting scope checking.
Scope checking Agda.Primitive
  visited: Agda.Primitive, Agda.Primitive.Cubical
  Already visited Agda.Primitive
Scope checking Agda.Primitive
  visited: Agda.Primitive, Agda.Primitive.Cubical
  Already visited Agda.Primitive
Finished scope checking.
Starting highlighting from scope.
Finished highlighting from scope.
Starting type checking.
Finished type checking.
Starting highlighting from type info.
Finished highlighting from type info.
Starting serialization.
Building interface...
  Already visited Agda.Primitive
  instantiating all meta variables
  interface complete
Finished serialization.
Considering writing to interface file.
Actually calling writeInterface.
Writing interface file /usr/share/agda-stdlib/_build/2.6.4.1/agda/Level.agdai.
Failed to write interface /usr/share/agda-stdlib/_build/2.6.4.1/agda/Level.agdai.
/usr/share/agda-stdlib/Algebra/Core.agda:13,1-30
/usr/share/agda-stdlib/_build/2.6.4.1/agda/Level.agdai: removeLink:
permission denied (Permission denied)

[UlfNorell]

Data.Nat is not up-to-date because the interface has not been decoded and options changed.

So Agda thinks that the options have changed, that's very mysterious.

[UlfNorell]

Can you upload Level.agdai here, and I'll see if I can figure out what the options in it are?

[jamesmckinna]

Two things (seem to) jump out at me from the OP, but apologies in advance if I have misunderstood something:

• is the library version 1.2.0 or 2.0; if the former, please use an up-to-date version, such as 2.0 released in December 2023; if already using that version, note that Everything.agda now resides under doc not src (and GenerateEverything, run from make setup should sort this out), so your agda +RTS -K1G -RTS -i . -i src Everything.agda may not work if you're not in the right directory; (check your *Makefiles and/or build scripts, and rerun those supplied with the library distribution?)
• if /usr/share/agda-stdlib/ isn't user-writeable, then agda's need to write to the _build subdirectory of that directory may fail, in any case...

So 'pre-building' compiled interfaces for the library seems a good idea (re the second point), but may fail if the first issue isn't addressed, because trying to (re)check Everything won't necessarily rebuild those interfaces as you seek to do...?

[UlfNorell]

The system agdai file has --warning=noUnsupportedIndexMatch, which you would expect since it's in the standard library agda-lib file (at least for the version I'm looking at), but the rebuild does not have the flag. Can you check the /usr/share/agda-stdlib/standard-library.agda-lib to see if it has the flag? Is it possible that the system installer sees a different agda-lib file from what you are using?

[kleinreact]

$ cat /usr/share/agda-stdlib/standard-library.agda-lib
name: standard-library
include: /usr/share/agda-stdlib

I also checked for the noUnsupportedIndexMatch flag in the installation scripts, but nothing in that direction is set or unset there explicitly.

It's basically this ebuild installing the library, except that I increased the version to 2.0, kept the _build folder on install and fixed the paths due to the agda-stdlib 2.0 updates. So it does not more than building GenerateEverything with cabal and then running the given Agda commands. Profiling is disabled for me, so no extra GHC flag is added.

[UlfNorell]

If you installed 2.0 then you absolutely should have --warning=noUnsupportedIndexMatch in the agda-lib file:

https://github.com/agda/agda-stdlib/blob/v2.0/standard-library.agda-lib#L4

Somehow you've managed to install a different (and incorrect) standard-library.agda-lib in /usr/share/agda-stdlib than the one used to compile the library.

[kleinreact]

Adding flags: --warning=noUnsupportedIndexedMatch fixes the problem.

Indeed, the Gentoo upstream package for agda-lib 1.7.2 uses some other standard-library.agda-lib, which is not taken from the repository. I haven't updated that file when updating to 2.0, so thanks a lot for pointing that out.

I can't say though, why it also was running into the same issue before updating to 2.0. I'm fine with staying on 2.0 for now, so this issue can technically be closed.

[UlfNorell]

1.7.2 also has the flag in the agda-lib file.