Migrate from ulex to sedlex

[XVilka]

Long story short - ulex is dying, mainstream depends on the camlp4, which is dead, fork depends on the camlp5, which seems dead too. This prevents from porting F* to more modern OCaml versions and dependencies versions.

See these links for more information:

• https://discuss.ocaml.org/t/camlp5-and-ocaml-4-08/3985/4
• Rename ulex-camlp5 into ulex ocaml/opam-repository#14351

Sedlex is an active maintained project by OCaml community: https://github.com/ocaml-community/sedlex

[catalin-hritcu]

@ad-l

[catalin-hritcu]

@avsm also strongly encourages us to get rid of the camlp4 dependency:
ocaml/opam-repository#14377 (comment)

[XVilka]

Related also FStarLang/karamel#138

[ad-l]

We considered moving to sedlex when we first implemented Unicode support but at that time sedlex had significant limitations (in particular whith custom implementations of lexing buffer). I'm happy to have another look and discuss this at the next F* meeting

[XVilka]

Note, the Kremlin PR was merged

[XVilka]

And the official Camlp4 deprecation announcement: https://discuss.ocaml.org/t/the-end-of-camlp4/4216

[XVilka]

Note, that 4.09 release will be ready quite soon, but camlp4 won't be available for that version.

[XVilka]

OCaml 4.09 was released and it comes without camlp4 support.

[XVilka]

OCaml 4.10 is going to be released soon and the first beta is already available. Obviously, still can't be used with camlp4.

[fangyi-zhou]

Is it being worked on? I can try to submit a PR if that's not the case

[catalin-hritcu]

@fangyi-zhou I've asked the F* team, and it seems no one is working on this. So patches welcome!

[XVilka]

@fangyi-zhou you can use the Kremlin commit as a reference in case there are issues with this task: FStarLang/karamel@4acd7cc

[fangyi-zhou]

It's more complicated than the kremlin commit because there is also the FStar.ULexing module that uses some APIs sedlex doesn't support.
I pushed my progress to https://github.com/fangyi-zhou/FStar/tree/sedlex

[XVilka]

@fangyi-zhou depending on what must be enhanced in Sedlex it might be useful to ask its developers or send a pull request https://github.com/ocaml-community/sedlex/issues

[catalin-hritcu]

Our Homebrew formula's deletion (#1938) is also a consequence of the camlp4/ulex dependency:
Homebrew/homebrew-core#49745

[fangyi-zhou]

Sorry I didn't manage to make a pull request. On a separate note, maybe replace ulex with ulex-camlp5 as a quick workaround?

[XVilka]

Quick workarounds tend to stay forever. IMHO, it's better to fix it properly. Nobody will fix ulex bugs in the future, there is no guarantee it will be compatible with the next OCaml version, etc.

[fangyi-zhou]

If you're happy to dig into why sedlex hangs on compilation, I'm happy to make the rest of the changes