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.

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

Agda 2.6.0 compatibility #2

Open
ice1000 opened this Issue Nov 14, 2018 · 5 comments

Comments

Projects
None yet
2 participants
@ice1000
Member

ice1000 commented Nov 14, 2018

No description provided.

@ice1000 ice1000 self-assigned this Nov 14, 2018

@ice1000

This comment has been minimized.

Member

ice1000 commented Nov 14, 2018

Checking Web.Semantic.Everything (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/Everything.agda).
 Checking Web.Semantic.DL.ABox (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox.agda).
 Checking Web.Semantic.DL.ABox.Interp.Meet (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Meet.agda).
  Checking Web.Semantic.DL.ABox.Interp.Morphism (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda).
   Checking Web.Semantic.DL.TBox.Interp.Morphism (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/TBox/Interp/Morphism.agda).
 Checking Web.Semantic.DL.ABox.Model (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda).
/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda:143,1-14
Don't know how to parse inb (f , I⊨A). Could mean any one of:
  inb (_,_ f I⊨A)
  inb (_,_ f I⊨A)
  inb (_,_ f I⊨A)
  inb (_,_ f I⊨A)
  inb (_,_ f I⊨A)
  inb (_,_ f I⊨A)
Operators used in the grammar:
  , (infixr operator, level 4) [_,_ (/home/ice/.cabal/share/x86_64-linux-ghc-8.4.3/Agda-2.6.0/lib/prim/Agda/Builtin/Sigma.agda:8,15-18)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox.agda:15,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp.agda:14,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda:25,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda:68,3-6)]
  , (infixr operator, level 5) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda:139,5-8)]
when scope checking the left-hand side inb (f , I⊨A) in the
definition of inb
@ice1000

This comment has been minimized.

Member

ice1000 commented Nov 14, 2018

Is Agda completely losing the ability to use type inference to resolve overloaded operators? @UlfNorell Is this a language change?

@ice1000

This comment has been minimized.

Member

ice1000 commented Nov 14, 2018

  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
Operators used in the grammar:
  , (infixr operator, level 4) [_,_ (/home/ice/.cabal/share/x86_64-linux-ghc-8.4.3/Agda-2.6.0/lib/prim/Agda/Builtin/Sigma.agda:8,15-18)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox.agda:15,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp.agda:14,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda:25,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda:68,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Category/Morphism.agda:25,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Category/Morphism.agda:30,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Category/Morphism.agda:77,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Category/Object.agda:13,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Integrity.agda:44,5-8)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Integrity.agda:65,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Integrity.agda:84,5-8)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/KB.agda:10,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/TBox.agda:14,3-6)]
  , (infixr operator, level 5) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda:139,5-8)]
when scope checking the left-hand side
pipe (J , j) (K , k) (J≲K , j≲k) in the definition of pipe

@ice1000 ice1000 removed their assignment Nov 14, 2018

@ice1000

This comment has been minimized.

Member

ice1000 commented Nov 14, 2018

My Agda compiler is built from 2d980891f570cf4a50b8e8843eb9c5269b4d888e commit in the compiler repo

@gallais

This comment has been minimized.

Member

gallais commented Nov 14, 2018

If you make sure that all _,_ have the same fixity level then it should fix the issue, I believe.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment