Skip to content

Conversation

mtzguido
Copy link
Member

They cannot be removed from the fsti as they are needed for extraction, but marking them private makes them unaccessible to users, instead of just warning.

They cannot be removed from the fsti as they are needed for extraction,
but marking them private makes them unaccessible to users, instead of
just warning.
@gebner
Copy link
Contributor

gebner commented Jun 27, 2025

I'm not sure if this buys us much. There are also legitimate reasons to call Reference.alloc, e.g. when providing a (non-extracted) model implementation--such as for the nested-reference-encoding that we're trying out for structures. You can locally undeprecate alloc, but friending is global for the whole module.

They cannot be removed from the fsti as they are needed for extraction

Since this took me a second to figure out:

  1. let mut gets parsed as a Tm_WithLocal.
  2. Pulse.Extract.Main turns this Tm_WithLocal into a call to Reference.alloc.
  3. ExtractPulse then translates this Reference.alloc call into a stack initialization.

And the declaration in the fsti is necessary for the F* extraction in step 2.5, where we need the type of Reference.alloc to determine its ML type.

@mtzguido
Copy link
Member Author

You can locally undeprecate alloc, but friending is global for the whole module.

What about moving alloc/__alloc to a standalone module? I think it's really bad experience that the usual open Pulse brings in the deprecated, unsound alloc into scope.

@mtzguido
Copy link
Member Author

Oh I misunderstood your comment I think, friending is global for the client.

@gebner
Copy link
Contributor

gebner commented Jun 27, 2025

What about moving alloc/__alloc to a standalone module?

I'd prefer that over friending to be honest.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants