is using Parsec in nightly recommended?

Stream: new members

[Shubham Kumar 🦀 (he/him)]

I see that Parsec was moved from Lean.Data.Parsec to Std.Internal.Parsec and many functions like pchar, etc aren't part of this. I do see charLit and nameLit in Lean.Parser.Parser exists which does look it has a similar function.

Is this the recommended way to move forward if I want to use Parsec like functions?

Thanks!

[Alexandre Rademaker]

In the last release, my code below is now broken...

def parseSpace : Parsec String := do
  let a ← many (satisfy $ fun c => c.isWhitespace)
  return a.asString

The error says

function expected at
  Parsec
term has type
  ?m.76

What precisely changed in the Parsec? It seems it needs one extra argument, am I right? Any documentation about this new implementation?

[Kyle Miller]

Here's the breaking changes entry in the release notes:

The Parsec library has moved from Lean.Data.Parsec to Std.Internal.Parsec. The Parsec type is now more general with a parameter for an iterable. Users parsing strings can migrate to Parser in the Std.Internal.Parsec.String namespace, which also includes string-focused parsing combinators. (#4774)

You should be able to use Parser instead of Parsec.

[Kyle Miller]

(ping @Alexandre Rademaker)

[Alexandre Rademaker]

Wow.. I didn't notice the Parser name vs Parsec in the line

abbrev Parser (α : Type) : Type := Parsec String.Iterator α

thank you...