I think --experimental-transport-indices is a good name: not too technical, describes exactly what goes wrong otherwise (substituting an index by a path will get stuck).

Is the idea that inductive families would not be allowed unless this flag is used, or would the flag only affect the extra clauses? In the former case the flag should presumably also be required to use inductive families when --without-K is used.

Without the flag, we'd skip:

• Generating transpX for indexed families
• Generating trX-trX clauses, trX-hcomp clauses, trX-con clauses when matching on indexed families

That is: without the flag, we have 2.6.2.2's status quo when it comes to indexed families in --cubical. They're allowed, but transport on them doesn't compute.

Something to keep in mind: #5448

Nisse 2022-08-31: The flag should be coinfective and turned on in the builtin modules.
Amelia: --cubical and --safe should imply the flag.
Nisse: The flag should be enabled in the standard library.

Here's a summary of our discussion on this topic on 2022-08-31 (@jespercockx @andreasabel @nad @UlfNorell) to make sure we're all on the same page (and to get user feedback, of course).

First, background:

1. Agda should have a flag that makes it compatible with univalent type theory, without bringing in anything cubical. In version 2.6.2.2, this is called --without-K.

2. Cubical Agda is a thing that exists. More importantly, Cubical Agda needs to be able to sneakily invite itself to modules, because any Agda code that could in the future be loaded by one using --cubical needs to have cubical stuff to work.

Side note: I'm calling the generated bits of code "cubical stuff" for short since the actual details of what needs to be generated are not relevant and are basically internal implementation details.

3. It should be possible to write code that is compatible with, but not allowed to make use of, cubical features.

Originally we had a proposal (#5843) to stratify the flags like so:

• without-K limits pattern matching, changes the termination checker, and changes how indices are counted towards the sorts of indexed types.
• cubical-compatible implies without-K and additionally tells Agda to generate cubical stuff for this module.
• cubical and erased-cubical are unchanged.

These flags got conflated because of the fix for #5448: When cubical clauses aren't generated, Agda accidentally allows you to generate code that is invalid wrt erasure. To be explicit, in

subst : (@0 P : A → Set p) → x ≡ y → P x → P y
subst _ refl p = p

the semantics of without-K should be that the use of a substitution derived from splitting on refl to under P should count as a use: the path p may have content, after all. When cubical stuff is generated, we get a literal use in one of the generated clauses, so that Agda correctly rejects this code:

subst {A} {P} {x} {y} (transpX (p : Path y' y) (r : x ≡ y')) z
  = transp (\ i -> P (p i)) i0 (subst {A} {P} {x} {z} r z)

Proposal:

Let's split without-K and cubical-compatible again. These are the interactions, or at least the ones I can think of:

• cubical-compatible should imply without-K.

• cubical-compatible is coinfective. For onlookers this means that if A is cubical-compatible and A imports B, then it's an error for B not to be cubical-compatible.

• As today, cubical is infective, but it is changed to imply the new the coinfective cubical-compatible.

Modules that are without-K can not be imported from cubical or cubical-compatible code, because from the perspective of cubical-compatible, those modules are incomplete (e.g. they are missing transpIx definitions, which are required in the client module for the coverage checker).

An immediate effect is that this re-breaks #5448, which will require a fix independent of cubical stuff.

To clarify, is the intent that:

1. --without-K is ideally supposed to exclude all features that are incompatible with univalence (even if it doesn't successfully do that today), and
2. Anyone writing code that might conceivably be imported by someone else's cubical code in the future must explicitly declare that using --cubical-compatible?

From this user's perspective, splitting --without-K and --cubical-compatible feels like exposing undesirable implementation details. As a user of univalent type theory who is not deeply versed in cubical type theory and doesn't use it regularly, it wouldn't have occurred to me at first that my definitions need to have "cubical stuff added" in order to be usable by someone doing cubical type theory. (After thinking about it, the reason is clear, but at an intuitive level one feels that definitions in Book HoTT should just "make sense" in cubical type theory without needing to be changed.)

Given this proposal, under what circumstances should I choose to use --without-K rather than --cubical-compatible? Is it because I might want to avoid the extra overhead of generating cubical stuff?

On the other side, if I'm using cubical agda and I want to import someone else's library who wrote it using --without-K, what do I have to do? If I just go change all the --without-K flags to --cubical-compatible, am I guaranteed that their library will still compile? Can I do that "globally" in some way without modifying their code?

I kind of feel like the ideal setup would be for Agda to check whenever importing a file from a --cubical file whether the file to be imported was compiled with cubical stuff, and if not, recompile it right then to add the cubical stuff needed. Then there wouldn't be a need for --cubical-compatible. I expect probably that is impossible, however.

On the other side, if I'm using cubical agda and I want to import someone else's library who wrote it using --without-K, what do I have to do? If I just go change all the --without-K flags to --cubical-compatible, am I guaranteed that their library will still compile? Can I do that "globally" in some way without modifying their code?

You can add the --cubical-compatible flag to the .agda-lib file of the library you want to use, so you'd only need to change a single file in the library. Ideally this would always succeed (but take a bit more time since it has to generate the cubical clauses), but this is not something we can guarantee at the moment. Also --cubical-compatible might generate error messages that mention the generated cubical clauses, which --without-K wouldn't (again, ideally you'd never see any errors in the generated clauses, but this is currently not something we can guarantee easily either).

There are a fair number of subtleties around elaboration of modules that could be loaded from Cubical Agda, particularly around indexed inductives — but, yes, also internal implementation details, as you mention.

In the development version of Cubical Agda, indexed inductive types have "formal transport along indices" as an additional constructor†, in exactly the same way that higher inductive types have "formal homogeneous compositions". Correspondingly, pattern-matching definitions need to handle these extra clauses. The part about HITs and their extra clauses is already true in the released version, for what it's worth, but it's not observable by non---cubical users because.. well, they don't have HITs.

We can imagine making switches for all of the following:

1. Should we disable the K rule? In both 2.6.2.2 and master, this is mandatory for using any Cubical features, and it's also used by people who want to explore other HoTT-like theories (or want to be agnostic towards K).

2. Should we treat indexed inductives as having formal transports, and thus generate the extra clauses? In master, this is required to be done in module compatible with Cubical Agda, since users of Cubical Agda depend on this.

3. Should we enable cubical features? This one is self-explanatory: It's --cubical and --erased-cubical. Note that cubical implies the coinfective without-K, so --cubical modules can load any module defined --without-K, and only those modules.

Conflation of (1) and (2) leads to a couple infelicities:

• Sometimes, generation of internal clauses will cause errors. This is a bug! But, even if we sometimes ship buggy software, there's at least an effort to ship buggy software that isn't confusing: The original proposal for renaming --without-K comes from @MatthewDaggitt running into cubical errors in the standard library, which is cubical-agnostic.

• Users of Agda which want to understand the precise features used in their code would like to control whether or not their code elaborates to anything cubical, especially if they themselves did not ask for --cubical. Initially I thought this complaint was silly, but I understand it better now: Agda's type theory is already nebulous enough without sneaking in changes to elaboration that aren't published anywhere, and aren't described in the published papers that describe the features they are using.

Now, speaking hypothetically, there is another very good reason to separate (1) and (2): Issue #3750. If we, in the future, implement a variant of Cubical Agda that is either agnostic towards or enforces K (this could be as simple as "cubical agda, but don't let people use Glue", or as complex as full-on XTT), we would still need to generate formal hcomp (for quotient-inductive types) and formal transp (for indexed types).

Treating (1) and (2) as one and the same means that, in this hypothetical future, users can't choose for their modules to be "agnostic towards implementation of K": Either you disable K (meaning your module would be loadable from --cubical and "--xtt", but couldn't.. make use of K) or you make use of K, but forbid your module from being used with --xtt.

Yet another hypothetical future change to Agda (which, to be clear, is even less likely to happen than --xtt, but it is interesting to ponder from a semantics POV) would be making hcomp in all inductive types formal, as IIRC is done in cooltt. Thus, even if you don't use indexed types (the current big sticking point), your "cubical compatible" modules would need to have cubical machinery.

† It's not a literal constructor but if you're knowledgeable enough about the implementation to tell the difference, please suspend your disbelief 🙂

I see and agree with the arguments for a --without-K that doesn't generate cubical stuff. I would also be annoyed if I were doing a development in Book HoTT and saw errors talking about cubical things. I just wish it weren't necessary for the author of a library to decide whether to make it compatible with cubical (or for the person using cubical to manually modify the library code, or even just the .agda-lib file, in order to import it).

I kind of feel like the ideal setup would be for Agda to check whenever importing a file from a --cubical file whether the file to be imported was compiled with cubical stuff, and if not, recompile it right then to add the cubical stuff needed. Then there wouldn't be a need for --cubical-compatible.

I suggested the same, using different build trees for build with or without cubical stuff, to avoid overwriting previous build efforts when you switch between main files that do --cubical or not --cubical. @nad was against this, but I forgot why.

I currently use --cubical/--erased-cubical when I use cubical features, and otherwise mostly --without-K, and I can use both variants in a single development. With the suggested setup, if I work on a file X.agda that takes a long time to type-check and that uses --without-K, if I then switch to a file that uses --erased-cubical and that imports X.agda, then X.agda would be type-checked again, and this could take minutes. Furthermore, if X.agda does not satisfy the extra rules imposed by the cubical variants of Agda, then I would get a type error in X.agda. However, in order to debug that type error I could not work locally on X.agda, unless I temporarily switched from --without-K to --erased-cubical or --cubical in that file.

I think the main problem with the current setup is that generated code (related to Cubical Agda) can leak into error messages (even for people who do not use Cubical Agda). If we could implement a fix for issue #5448 that produced readable error messages, then I don't think there would be a strong need for --cubical-compatible (except perhaps if the cubical stuff slows Agda down too much).

@plt-amy, your latest proposal does not mention --experimental-transport-indices, is that option still on the table?

Would it be possible to do both? Include --cubical-compatible for people in Nils' situation, but also automatically recompile --without-K files cubically when importing them from --cubical ones?

The option --cubical-compatible has to be used in all imported modules. I think we should encourage people writing reusable libraries to use this option.

Theoretically, we'd also need a flag --erased-cubical-compatible for modules that are compatible with --erased-cubical but not with --cubical (see #6114). This flag would generate the extra definitions needed for cubical, but mark them as erased. My motivation for this is that I'd like to use cubical to prove things about code written for Agda2Hs, but there are datatypes in the Agda2Hs prelude that should only be accepted by --erased-cubical but not by --cubical.

Where do I find the list of all options and their defaults?

You can use agda --help and agda --help=warning to see most options.

Thanks. Is that the only place "most" options are documented?

All options are documented at https://agda.readthedocs.io/en/v2.6.2.2/tools/command-line-options.html

Except for some that aren't, like the extra flags that can be passed to -v I learned about recently such as import.chase.

Perhaps --exact-split should be on by default? I've seen many students struggling with the fact that their definitions don't give definitional equalities.

I agree, except that when I first introduced the flag some people complained VERY LOUDLY about even just having a light grey background for the offending clauses.

All options are documented at https://agda.readthedocs.io/en/v2.6.2.2/tools/command-line-options.html

No, some are missing, including at least --prop, --guarded, and --two-level.

Is that the only place "most" options are documented?

Regarding "most": One option is missing, --ignore-all-interfaces, but that option is not supposed to be used by regular users.

@mikeshulman wrote:

Except for some that aren't, like the extra flags that can be passed to -v I learned about recently such as import.chase.

Agda does not have conscious knowledge of the verbosity hierarchy. You can pass in anything with -v, unknown verbosity strings just do not have any effect. It would be cleaner to have an explicit catalogue of verbosity strings, but this is tedious for the developers; and these are only for debug printing.
Apparently you found import.chase useful, so consider making a proposal to make this verbosity string official (and maybe others).

What is still open here seems to be @nad's planned changelog on performance:

• Separate flags for "compatible with univalence" and "compatible with Cubical Agda" #6049 (comment)

@nad wrote:

I plan to add something like the following:

Nisse, are you still intending this? Otherwise, we can close this issue.

I plan to do this just before the next release candidate, or just before the release.

@nad If you still want to get this into the release I suggest you do it soon.

Changes to the code can affect Agda's performance. I plan to do this once all such changes have landed.

Now I got the following numbers:

• Agda 2.6.3, compiled with GHC 9.4.3, with -fenable-clustering-counting and -foptimise-heavily enabled, for the standard library (commit c5f42e1fb86b964dfe2558e103f2f4f662e553b3 with --cubical-compatible enabled in most modules), the worst of two runs (the other one was about nine seconds faster):

   776,232,581,760 bytes allocated in the heap
    93,021,091,928 bytes copied during GC
     1,509,595,560 bytes maximum residency (156 sample(s))
         5,174,872 bytes maximum slop
              2282 MiB total memory in use (0 MB lost due to fragmentation)
  
                                       Tot time (elapsed)  Avg pause  Max pause
    Gen  0     184608 colls,     0 par   74.649s  74.733s     0.0004s    0.0263s
    Gen  1       156 colls,     0 par   10.780s  10.781s     0.0691s    0.6478s
  
    TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)
  
    SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)
  
    INIT    time    0.000s  (  0.000s elapsed)
    MUT     time  232.692s  (231.408s elapsed)
    GC      time   85.430s  ( 85.514s elapsed)
    EXIT    time    0.001s  (  0.008s elapsed)
    Total   time  318.123s  (316.930s elapsed)
  
    Alloc rate    3,335,884,664 bytes per MUT second
  
    Productivity  73.1% of total user, 73.0% of total elapsed
  

• Agda 2.6.3, compiled with GHC 9.4.3, with -fenable-clustering-counting and -foptimise-heavily enabled, for the standard library (commit e873a786a3cfe76367a5d0a1d9b2da3c0cdf6af1 without --cubical-compatible), the worst of two runs (the other one was similar):

   581,486,402,304 bytes allocated in the heap
    54,256,390,544 bytes copied during GC
     1,174,244,880 bytes maximum residency (117 sample(s))
         4,783,496 bytes maximum slop
              1894 MiB total memory in use (0 MB lost due to fragmentation)
  
                                       Tot time (elapsed)  Avg pause  Max pause
    Gen  0     138162 colls,     0 par   48.831s  48.885s     0.0004s    0.0242s
    Gen  1       117 colls,     0 par    4.643s   4.643s     0.0397s    0.1983s
  
    TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)
  
    SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)
  
    INIT    time    0.001s  (  0.000s elapsed)
    MUT     time  180.140s  (179.008s elapsed)
    GC      time   53.474s  ( 53.528s elapsed)
    EXIT    time    0.001s  (  0.004s elapsed)
    Total   time  233.616s  (232.540s elapsed)
  
    Alloc rate    3,227,963,050 bytes per MUT second
  
    Productivity  77.1% of total user, 77.0% of total elapsed
  

• Agda 2.6.2.2, compiled with GHC 9.4.3, with -fenable-clustering-counting and -foptimise-heavily enabled, for the standard library (commit 4b7e69b22ec698716f323fc24fc6bd1305ed47df), the best of two runs (the other one was similar):

   815,837,786,360 bytes allocated in the heap
    71,253,738,216 bytes copied during GC
     1,136,954,952 bytes maximum residency (164 sample(s))
         2,049,984 bytes maximum slop
              1953 MiB total memory in use (0 MB lost due to fragmentation)
  
                                       Tot time (elapsed)  Avg pause  Max pause
    Gen  0     192219 colls,     0 par   81.075s  81.172s     0.0004s    0.0216s
    Gen  1       164 colls,     0 par    6.892s   6.952s     0.0424s    0.2266s
  
    TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)
  
    SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)
  
    INIT    time    0.001s  (  0.003s elapsed)
    MUT     time  265.432s  (264.177s elapsed)
    GC      time   87.968s  ( 88.124s elapsed)
    EXIT    time    0.001s  (  0.007s elapsed)
    Total   time  353.402s  (352.310s elapsed)
  
    Alloc rate    3,073,618,868 bytes per MUT second
  
    Productivity  75.1% of total user, 75.0% of total elapsed
  

The speedup in 2.6.3 is nice, but it's rather encouraging me to stick with --without-K in agda-categories rather than switching to --cubical-compatible.

The speedup in 2.6.3 is nice, but it's rather encouraging me to stick with --without-K in agda-categories rather than switching to --cubical-compatible.

That would mean that one cannot import the code from Cubical Agda. Could you use --without-K when developing new code, but switch to --cubical-compatible before releasing it?

Here are some more statistics on time efficiency using time agda AllModules.lagda with https://github.com/martinescardo/TypeTopology

In a 2020 MacBook Air M1:

• With the current version of Agda: 8min
• With the release candidate: 4min

In a 2017 Dell Latitude laptop with a core i5 Intel processor:

• With the current version of Agda: 13m35
• With the candidate release version: 8m47s.

For the release candidate we used ghc 9.4.3, and for the current version we used ghc 8.10.7, in both setups (for historical reasons).

Note that @martinescardo 's measurements use --without-K and not --cubical-compatible. Though how much is due to Agda and how much to GHC is unclear.

Nevertheless, the speedup is quite remarkable.