Maybe --cubical-compatible is a mistake for stdlib 2.0?

[JacquesCarette]

See this issue about Agsy failing, and --without-K being the fix.

If cubical truly want to use stdlib, there is likely a need for a concerted effort to make them compatible (such as: remove the duplication!)

[andreasabel]

With Agda 2.6.3, if you do not want to use cubical features, there is an advantage to use std-lib 1.7.1 (--without-K) over 1.7.2 (--cubical-compatible, but otherwise identical to 1.7.1).

I agree that I want the option of not having the cubical compatible definitions for uses of the standard library if I do not want to do anything cubical. It is faster to build (20-25% I think) and it is more robust, as the linked issue shows.

Ideally, one would just have --without-K in the files of the std-lib, but then the possibility to add a flag to the standard-library.agda-lib file that switches to --cubical-compatible where possible. That means, --with-K in a file should override a --cubical-compatible given globally for the project.
This would need changes in Agda to the flag handling.

The alternative would be to release two versions of the standard library, one --without-K and one --cubical-compatible, but I think this was what we wanted to avoid...

[gallais]

Do we have cubical customers (independently from the cubical lib)?
E.g. does @nad use the stdlib in combination with cubical features?

[jamesmckinna]

This is/appears to be currently a problem for all users during development (until and unless Agsy is upgraded to incorporate richer search spaces) but only for library developers/maintainers when merging PRs.

Accordingly I think, but perhaps more fieldwork is required to confirm this, that the least worst solution/advice to users might be:

• use --without-K during development (especially if using C-h a) if cubical features are not used;
• use --cubical-compatible only when merging into the library.

Going backwards to v1.7.2 would, I think, be a terrible mistake given the enormous amount of work over the last 2+ years in preparing v2.0 for (eventual) release.
.

[jamesmckinna]

(And, correspondingly, imagining a time in the future when cubical features are more robust/just as efficient to typecheck... ;-))

[jamesmckinna]

BTW/FWIW, I think that PR #1935 was premature, (we might at least have had a shot at releasing 2.0 before proceeding), but rolling it back would be ... also a mistake.

I'm 'happy' to take a performance hit on typechecking --without-K only code, for the sake of maintaining a single active (and compatible!) Agda and stdlib release, even if that may require patience and some intelligent compromise.

[nad]

E.g. does @nad use the stdlib in combination with cubical features?

Yes, I do.

We stopped supporting Agsy a long time ago. Another way to fix the problem would be to remove the Agsy code from Agda (perhaps in favour of Mimer).

[andreasabel]

It is not only Agsy which is affected by --cubical-compatible.
E.g. Agda 2.6.3 also has an issue with extended lambdas:

• fixup: don't reify DefP clauses when printing an extended lambda agda#6580

I am afraid more leaks of cubical stuff into regular Agda via --cubical-compatible will be uncovered in the future.
Thus, I lean towards a "hardware" separation of cubical from non-cubical Agda, via using --without-K rather than --cubical-compatible as the default. (But, as I said before, we would need to change Agda so that --with-K can override --cubical-compatible.)

[jamesmckinna]

Uh-huh, I see (more or less). But does my suggestion work in advance of any of these proposed changes being made?

[andreasabel]

@jamesmckinna wrote:

Accordingly I think, but perhaps more fieldwork is required to confirm this, that the least worst solution/advice to users might be:

• use --without-K during development (especially if using C-h a) if cubical features are not used;
• use --cubical-compatible only when merging into the library.

I take this is the suggestion. To make this work, one would need an easy way to switch the library between these two modes.
Currently, this is a 1000 file modification, as 1000 files have {-# OPTIONS --cubical-compatible #-} in the preamble which cannot be overwritten with giving --without-K in the .agda-lib file or at the command line (if I am not mistaken).

[jamesmckinna]

Hmmm, perhaps I have misunderstood something: if I import a library module marked as --cubical-compatible, I can still make my client module --without-K without a warning (the converse does generate a warning). Quick check: is this semantics correct?

But if I subsequently try to merge such a module into the library, then make test will complain (because Everything{Safe}.agda is now the 'client', attempting to import a --without-K module into a --cubical-compatible context...
EDITED that said, Everything{Safe}.agda make no reference to either flag, so I am somewhat stumped as to why make test should complain... ah I see the error seems to be being thrown by code in GenerateEverything.classify.

[jespercockx]

I take this is the suggestion. To make this work, one would need an easy way to switch the library between these two modes.
Currently, this is a 1000 file modification, as 1000 files have {-# OPTIONS --cubical-compatible #-} in the preamble which cannot be overwritten with giving --without-K in the .agda-lib file or at the command line (if I am not mistaken).

Would it make sense to split the library into two folders, each with their own .agda-lib file? That way it would be a lot easier to switch between --without-K and --cubical-compatible for the part that does not use --with-K.

[nad]

Ideally, one would just have --without-K in the files of the std-lib, but then the possibility to add a flag to the standard-library.agda-lib file that switches to --cubical-compatible where possible.

I don't think this is ideal. I don't want to rely on a locally patched variant of a library.

I think that at some point you suggested something like the following:

• Use separate build directories for Cubical Agda and non-cubical Agda.
• When importing non-cubical code from cubical code, build the non-cubical code with the extra cubical stuff, and put the interfaces in a Cubical Agda build directory.

With this approach we could merge --without-K and --cubical-compatible. The approach could in some cases lead to unnecessary waiting for users:

• You work on module M1, which does not use Cubical Agda. The module finishes type-checking.
• You switch to module M2, which uses Cubical Agda, and imports M1. Before you can start working Agda has to type-check M1 from scratch, which in some cases could take significant time.

However, I still think this is preferable to making the (unpatched) standard library unusable for users of Cubical Agda.

[uhbif19]

Use separate build directories for Cubical Agda and non-cubical Agda.

Why could not that be single directory, just tracking existence of additional "cubical" info in individual files instead? Like for non-cubical usage that info could be just dropped/tree-shaked while compiling. And otherwise AFAIU having that info during compilation is okay in without-K case.

[jamesmckinna]

Suggest we close, and accept that this particular ship has sailed?

There are various other issues on the main tracker concerning performance... but such things also tend to get solved by waiting long enough (sic)...

[MatthewDaggitt]

Closing as suggested. I agree that we want to avoid duplicating the library at all costs.

But, as I said before, we would need to change Agda so that --with-K can override --cubical-compatible

I agree with @andreasabel that this seems like the best upstream fix.