Internal.Parsec.String.Parser

Stream: general

[Asei Inoue]

import Lean

open Std.Internal.Parsec
open Std.Internal.Parsec.String

structure DimacsHeader where
  numVars : Nat
  numClauses : Nat

def Parser.dimacsHeader : Parser DimacsHeader := do
  skipString "p cnf "

  let numVarsStr ← many1Chars (satisfy Char.isDigit)
  let numVars := numVarsStr.toNat!

  skipString " "
  let numClausesStr ← many1Chars (satisfy Char.isDigit)
  let numClauses := numClausesStr.toNat!

  return { numVars, numClauses }

#eval
  let result := Parser.run Parser.dimacsHeader "p cnf 1200 14"
  match result with
  | Except.ok header => s!"numVars: {header.numVars}, numClauses: {header.numClauses}"
  | Except.error err => s!"Error: {err}"

[Asei Inoue]

Here is a code example using Std.Internal.Parsec.String.Parser.

[Asei Inoue]

I want to use a Parser combinator in Lean and I've found Std.Internal.Parsec.String.Parser.
But it is under Std.Internal namespace.
This is not stable or not recommended to use by user?

[Asei Inoue]

why is it placed under internal namespace?

[Henrik Böving]

This is not stable or not recommended to use by user?

Not stable and thus not recommended for serious use at the moment yes

[Asei Inoue]

ok thanks

[Asei Inoue]

is there plan to make it stable?

[Henrik Böving]

Not in the near term. It mostly exists because we have things that need high performance parsing internally, such as the LRAT checker, but there are currently no direct plans to stabilize it.

[Asei Inoue]

Thank you Henrik!

[Matej Penciak]

I've been using the parser combinator library https://github.com/fgdorais/lean4-parser a lot in my personal projects. I think it's a good alternative to Std.Internal.Parsec

[Asei Inoue]

lean4-parser will be maintained in the future?