cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
235 stars 34 forks source link

Newlines should always be inserted between subsequent warnings #32

Closed JasonGross closed 3 years ago

JasonGross commented 3 years ago
!! Warning: Unexpected token during syntax-highlighting: '₁'
!! Alectryon's lexer isn't perfect: please send us an example.
!! Context:
        ...carriers_subalgebra A P t &
          in_class (Φ t) x (def_inc_subalgebra A P t y)}
        ∥₋₁./theories/Classes/orders/nat_int.v:176: (WARNING/2) Long line: 'We axiomatize the order on the naturals and the integers as a non trivial' (73 characters)

at https://github.com/HoTT/HoTT/runs/2353786837?check_suite_focus=true#step:5:2547

cpitclaudel commented 3 years ago

Are you running concurrently, or is it maybe that stderr is getting mixed with stdout?

JasonGross commented 3 years ago

It could be that stderr is getting mixed with stdout. But shouldn't both of these be output on stderr?

I'm only running one instance of alectryon; I pass it a list of a couple hundred .v files.