Highlighting bug extension types

[fredrik-bakke]

While refactoring code today, I noticed some strange highlighting. Here is a screenshot, see the selected code:

[fizruk]

Can you please also provide the text version for testing?

[fredrik-bakke]

My apologies! Here:

#def is-equiv-fibered-map-square-sigma-over-prod
  ( extext : ExtExt)
  ( A : U)
  ( Aisdiscrete : is-discrete A)
  ( x y z w : A)
  ( f : hom A x y)
  ( g : hom A z w)
  ( p : x = z)
  ( q : y = w)
  : is-equiv
    ( prod-transport A A (hom A) x z y w p q f = g)
    ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
      [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
				((t === 1_2) /\ Δ¹ s) |-> g s ,
				(Δ¹ t /\ (s === 0_2)) |-> (arr-eq A x z p) t ,
				(Δ¹ t /\ (s === 1_2)) |-> (arr-eq A y w q) t ])
    ( fibered-map-square-sigma-over-prod extext A Aisdiscrete x y z w f p q g)
  :=
    fibered-map-is-equiv-bases-are-equiv-total-map-is-equiv
      ( x = z)
      ( hom A x z)
      ( y = w)
      ( hom A y w)
      ( \ p' q' -> (prod-transport A A (hom A) x z y w p' q' f) = g)
      ( \ h' k' ->
        ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
          [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
            ((t === 1_2) /\ Δ¹ s) |-> g s ,
            (Δ¹ t /\ (s === 0_2)) |-> h' t ,
            (Δ¹ t /\ (s === 1_2)) |-> k' t ]))
      ( arr-eq A x z)
      ( arr-eq A y w)
      ( \ p' q' ->
        fibered-map-square-sigma-over-prod
          ( extext)
          ( A) (Aisdiscrete)
          ( x) (y) (z) (w)
          ( f)
          ( p')
          ( q')
          ( g))
      ( is-equiv-square-sigma-over-prod extext A Aisdiscrete x y z w f g)
      ( Aisdiscrete x z)
      ( Aisdiscrete y w)
      ( p)
      ( q)

Turns out there's a mix of tabs and spaces! Changing tabs to spaces seems to resolve the issue.

[fizruk]

I was able to reproduce on this code:
https://github.com/emilyriehl/yoneda/blob/4eb0755ab3ac1acb84805a09fc234399ee97e195/src/simplicial-hott/07-discrete.rzk.md?plain=1#L522-L538

Interesting, this is some bug in the semantic highlighting, locations are not computed correctly.

Thanks for reporting!

[fredrik-bakke]

Just to make sure, did you see my comment about tabs vs. spaces?

[fizruk]

Turns out there's a mix of tabs and spaces! Changing tabs to spaces seems to resolve the issue.

Wow, good catch! We need to suggest to always have spaces, not tabs. @aabounegm is it possible to have this automatically turned on/suggested within vscode-rzk?

[aabounegm]

Yes, it should be possible to override the settings by adding the following to package.json:

{
  "configurationDefaults": {
    "[rzk]": {
      "editor.insertSpaces": true
    }
  }
}

But I think the user's own settings will take precendence. I need to test it first.

We can also define our own formatter that would simply replace tabs with spaces for now, but that also depends on the users enabling it.

[fizruk]

We can probably at least warn if the user has tabs in the file?

[aabounegm]

Yes, that should also be possible. I will need to find the most appropriate provider (or just use the existing semantic highlighting one) to get access to the document content, but it should be simple.

[fizruk]

I think this is no longer an issue with semantic highlighting and #71.