Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

allow OCaml < 4.10 for fstar dev-repo #16684

Conversation

tahina-pro
Copy link
Contributor

Requested by @catalin-hritcu

The current opam packages for F* do not allow OCaml >= 4.08. However, the latest F* master does compile with OCaml < 4.10.
Thus, this pull request is meant to make opam pin fstar --dev-repo work for OCaml < 4.10, as documented at https://github.com/FStarLang/FStar/blob/3025f90e008f5793e3755ab115aecb4c17ab3714/INSTALL.md#opam-package

@camelus
Copy link
Contributor

camelus commented Jun 20, 2020

Commit: a885467

@tahina-pro has posted 6 contributions.

☀️ All lint checks passed a885467
  • These packages passed lint tests: fstar.0.9.7.0-alpha1

☀️ Installability check (+0)

@avsm
Copy link
Member

avsm commented Jun 22, 2020

This won't quite work, unfortunately, as it'll fail if you pin the released version of fstar with 4.10.

The solution to document for this is to commit the correct opam file into the f* repository, and then opam pin add fstar --dev should work, as opam will pick up that file and use its constraints.

@avsm avsm self-assigned this Jun 22, 2020
@tahina-pro
Copy link
Contributor Author

Sorry, I don't quite understand the first part of your comment. Could you please clarify? In fact, I do intend both the released version and --dev-repo to fail with OCaml >= 4.10, but only --dev-repo to succeed for OCaml >= 4.08 and < 4.10.

@XVilka
Copy link
Contributor

XVilka commented Jun 23, 2020

@tahina-pro shouldn't be FStarLang/FStar#1792 fixed first? I think ulex was abandoned and will not work with newer (>=4.10) OCaml.

@catalin-hritcu
Copy link
Contributor

catalin-hritcu commented Jun 23, 2020

@avsm @XVilka The purpose of this patch is not to support OCaml 4.10. It's to support 4.09.1, which is currently wrongly rejected for the dev repo, even though it's the version we would normally ask people to use these days.

@XVilka
Copy link
Contributor

XVilka commented Jun 23, 2020

Oh, sorry, I misread.

@avsm
Copy link
Member

avsm commented Jun 23, 2020

Right; this is what you need to do to support the master branch of F*:

  • add a fstar.opam file to your repository, with the correct metadata (that is "ocaml" {<"4.10.0"} for example)
  • run opam pin add fstar --dev to install it.

That's all. The --dev option will query the dev-repo field in the latest known version of fsharp in the opam-repo, use that to retrieve the master branch opam file, and subsequently use that for the metadata calculation.

This way, you don't need to backpatch existing fstar metadata versions. When the new fstar is ready to release, opam-publish or dune-release will just grab that latest metadata file in your trunk and use that for the new release.

@catalin-hritcu
Copy link
Contributor

Anil's suggestion indeed does the trick, so this pull request is no longer needed and can be safely closed. Many thanks.

@mseri
Copy link
Member

mseri commented Jun 28, 2020

Thanks!

@mseri mseri closed this Jun 28, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants