Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

1.7.2 errors with Agda 2.6.4 #2129

Closed
juhp opened this issue Oct 9, 2023 · 8 comments
Closed

1.7.2 errors with Agda 2.6.4 #2129

juhp opened this issue Oct 9, 2023 · 8 comments
Assignees
@andreasabel
Labels
bug
Milestone
v1.7.3

Comments

@juhp
Copy link

juhp commented Oct 9, 2023 •
edited
Loading

This may be my fault, but I tried to rebuild the Fedora agda-stdlib 1.7.2 package with Agda 2.6.4 and it seems to fail:

Reason: It relies on injectivity of the data constructor +_, which
        is not yet supported

when checking the definition of neg-antimono-≤
/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Rational/Properties.agda:726,1-732,97
warning: -W[no]UnsupportedIndexedMatch
This clause uses pattern-matching features that are not yet
supported by Cubical Agda, the function to which it belongs will
not compute when applied to transports.

Reason: It relies on injectivity of the data constructor -[1+_],
        which is not yet supported

when checking the definition of neg-antimono-≤
/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Rational/Properties.agda:805,1-824,80
warning: -W[no]UnsupportedIndexedMatch
This clause uses pattern-matching features that are not yet
supported by Cubical Agda, the function to which it belongs will
not compute when applied to transports.

Reason: It relies on injectivity of the data constructor false,
        which is not yet supported

when checking the definition of Data.Rational.Properties.with-2764
/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Rational/Properties.agda:805,1-824,80
warning: -W[no]UnsupportedIndexedMatch
This clause uses pattern-matching features that are not yet
supported by Cubical Agda, the function to which it belongs will
not compute when applied to transports.

Reason: It relies on injectivity of the data constructor true,
        which is not yet supported

when checking the definition of Data.Rational.Properties.with-2764
/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Rational/Properties.agda:1029,1-1047,80
warning: -W[no]UnsupportedIndexedMatch
This clause uses pattern-matching features that are not yet
supported by Cubical Agda, the function to which it belongs will
not compute when applied to transports.

Reason: It relies on injectivity of the data constructor false,
        which is not yet supported

when checking the definition of Data.Rational.Properties.with-3110
/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Rational/Properties.agda:1029,1-1047,80
warning: -W[no]UnsupportedIndexedMatch
This clause uses pattern-matching features that are not yet
supported by Cubical Agda, the function to which it belongs will
not compute when applied to transports.

Reason: It relies on injectivity of the data constructor true,
        which is not yet supported

when checking the definition of Data.Rational.Properties.with-3110
 Checking Data.Rational.Instances (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Rational/Instances.agda).
 Checking Data.Rational.Literals (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Rational/Literals.agda).
 Checking Data.Rational.Show (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Rational/Show.agda).
 Checking Data.Rational.Solver (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Rational/Solver.agda).
 Checking Data.Rational.Unnormalised (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Rational/Unnormalised.agda).
 Checking Data.Rational.Unnormalised.Solver (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Rational/Unnormalised/Solver.agda).
 Checking Data.Record (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Record.agda).
 Checking Data.Refinement (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Refinement.agda).
 Checking Data.Refinement.Relation.Unary.All (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Refinement/Relation/Unary/All.agda).
 Checking Data.Sign.Instances (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Sign/Instances.agda).
 Checking Data.Star.BoundedVec (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Star/BoundedVec.agda).
  Checking Data.Star.Nat (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Star/Nat.agda).
   Checking Relation.Binary.Construct.Always (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Relation/Binary/Construct/Always.agda).
    Checking Relation.Binary.Construct.Constant (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Relation/Binary/Construct/Constant.agda).
/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Star/Nat.agda:47,1-49,26
warning: -W[no]UnsupportedIndexedMatch
This clause uses pattern-matching features that are not yet
supported by Cubical Agda, the function to which it belongs will
not compute when applied to transports.

Reason: It relies on injectivity of the data constructor tt, which
        is not yet supported

when checking the definition of _∸_
/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Star/Nat.agda:47,1-49,26
warning: -W[no]UnsupportedIndexedMatch
This clause uses pattern-matching features that are not yet
supported by Cubical Agda, the function to which it belongs will
not compute when applied to transports.

Reason: It relies on injectivity of the data constructor tt, which
        is not yet supported

when checking the definition of _∸_
  Checking Data.Star.Decoration (/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Star/Decoration.agda).
/var/home/petersen/fedora/haskell/Agda-stdlib/BUILD/agda-stdlib-1.7.2/src/Data/Star/Decoration.agda:32,3-4
Set ℓ is not less or equal than Set p
when checking that the type I of an argument to the constructor ↦
fits in the sort Set p of the datatype.
Note: this argument is forced by the indices of ↦, so this
definition would be allowed under --large-indices.

Maybe only the last one is an actual error?
@MatthewDaggitt
Copy link
Contributor

Calling @plt-amy . Is there anything that has changed in cubical with indices in the last release?

@shhyou
Copy link
Contributor

shhyou commented Oct 10, 2023 •
edited
Loading

@plt-amy fixed large index issues of stdlib in #2030 to accommodate Agda 2.6.4 changes

@juhp
Copy link
Author

juhp commented Oct 10, 2023

So a new release is needed?

@andreasabel
Copy link
Member

andreasabel commented Oct 10, 2023 •
edited
Loading

Ah, indeed, I didn't test all of 1.7.1/2 with Agda 2.6.4, the parts of it that my projects used checked fine with Agda 2.6.4.
But indeed, some fixing is needed (and then a release of 1.7.3).
The minimal patch for 1.7.2 is to add to option --large-indices to the flags section of the .agda-lib file, but this is of course some overkill, as only some files need it.
The better way is to backport the fix that @plt-amy applied to the master of the std-lib, pointed out by @shhyou:

@jamesmckinna
Copy link
Contributor

Well, if we are talking about back-porting/back-patching v1.7.2, then I would advocate strongly for a revised version of #2125 for v.1.7.2 (or this hypothetical v1.7.3 which you allude to here) to supply enough Effect.* stubs to resolve issue #2124 ...

@jamesmckinna jamesmckinna mentioned this issue Oct 10, 2023
Closed
@andreasabel andreasabel self-assigned this Oct 10, 2023
@andreasabel andreasabel added this to the v1.7.3 milestone Oct 10, 2023
@andreasabel
Copy link
Member

@jamesmckinna: Good idea.

I'll give v1.7.3 a shot...

@andreasabel andreasabel mentioned this issue Oct 10, 2023
Closed
4 tasks
@MatthewDaggitt
Copy link
Contributor

Thanks @andreasabel !

@MatthewDaggitt
Copy link
Contributor

@juhp this is fixed in the just released v1.7.3. Apologies that this slipped under our radar.

@juhp juhp mentioned this issue Oct 16, 2023
Closed
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
bug
Projects
None yet
Milestone
v1.7.3
Development

No branches or pull requests
5 participants
@juhp @andreasabel @shhyou @MatthewDaggitt @jamesmckinna