Sexp parser seemingly broken in update from Lean 4.9 to 4.11

[ymherklotz]

We can't seem to be able to run auto with SMT solvers any more due to the lexer for the Sexp parser being seemingly broken.

When loading the tests Test/SmtTranslation/BoolNatInt.lean for example, with a freshly cloned and built lean-auto on the main branch, all auto runs fail with the following error:

‘auto’: getSexp :: Malformed (prefix of) input unsat

This seems to be due to the parser in our checkout failing, where the underlying issue seems to be the lexer. Adding the following lines below the parseSexp function in Auto/Parser/SMTSexp.lean results in a malformed result, which seems unexpected.

deriving instance Repr for LexVal
deriving instance Repr for Sexp
deriving instance Repr for PartialResult
deriving instance Repr for ParseResult

#eval parseSexp "unsat" ⟨0⟩ {}

I wasn't sure if the lexer was hand written or automatically generated and did not try to debug much further, but it seems like this should be parsed as an atom.

[PratherConid]

Sorry, I think I incorrectly modified List.mergeSort when I was correcting the termination proof for the update from 4.9 to 4.11. I've corrected the mistake and the parser should be working now.