dupuisf/bibtexquery

A simple command-line bibtex query utility written in Lean 4

bibtexquery's Issues

Some bugs in TeX diacritics and formatting code

I noticed some bugs in the code written by me, here is the record of them. Eventually I'll fix all of them.

• The TeX diacritics code written by me has potential bugs: if commands \$ and \backslash are processed (currently they are rejected directly), then they will breaking the following-up process. I think the proper solution is to store TeX AST.
• In LaTeX, some commands, e.g. \& and \#, preserves the trailing spaces, while \", etc. are not. But my current implementation removes all trailing spaces. This makes the space in John Wiley &Sons missing.
• The edition shows in a suboptimal place, and it will show some funny thing e.g. "3rd ed. edition", "1 edition", "Third Edition edition", "Reprint of the 1999 hardback ed. edition".
• Currently the \ and ~ are replaced by   in all fields, but this shouldn't be done in the fields url, doi, etc.

Parsec changes in recent lean-nightly (08-08-2024) break the build

I get the following error messages:

error: ././.lake/packages/BibtexQuery/././BibtexQuery/ParsecExtra.lean:21:57: type expected, got
  (Parsec α : Type → Type)
error: ././.lake/packages/BibtexQuery/././BibtexQuery/ParsecExtra.lean:26:61: type expected, got
  (Parsec α : Type → Type)
error: ././.lake/packages/BibtexQuery/././BibtexQuery/ParsecExtra.lean:32:28: type expected, got
  (Parsec Char : Type → Type)
error: ././.lake/packages/BibtexQuery/././BibtexQuery/ParsecExtra.lean:35:31: type expected, got
  (Parsec String : Type → Type)
error: ././.lake/packages/BibtexQuery/././BibtexQuery/ParsecExtra.lean:38:10: type expected, got
  (Parsec String : Type → Type)