Possible Verso–Mathlib conflict

Stream: mathlib4

[Palalansoukî]

I encountered an error that seems to result from a conflict between Verso and Mathlib (both v4.23.0):

import Mathlib
import VersoManual

open Verso.Genre Manual
open Verso.Genre.Manual.InlineLean

#doc (Manual) "Mathlib conflict?" =>
%%%
%%%

- A
* B
1. C

This triggers following errors:

linter Mathlib.TacticAnalysis.tacticAnalysis failed: operating on syntax without range
linter Mathlib.TacticAnalysis.tacticAnalysis failed: operating on syntax without range
linter Mathlib.TacticAnalysis.tacticAnalysis failed: operating on syntax without range

Removing either import Mathlib or the three bullet lists makes the error disappear. Also, adding set_option linter.tacticAnalysis false does not remove these errors.

It looks like Mathlib.TacticAnalysis runs on Verso syntax nodes without range info. How can I resolve this conflict?

[Anne Baanen]

This is a mistake in my original implementation of the tactic analysis linter, assuming that the syntax ranges have a relevant meaning. I have updated #28950 to completely remove this wrong check.

[Anne Baanen]

Thanks for pointing this out!