Skip to content

Conversation

@nikswamy
Copy link
Collaborator

@nikswamy nikswamy commented Nov 26, 2025

This PR provides --ext fly_deps, an option to scan and load dependences of a module incrementally, just before a single ast declaration is type checked, rather than scanning and loading a module's dependences up front, before the module is checked.

This is especially motivated by wanting to fix a wart in the interactive mode, where adding a dependence while working on a module required restarting the IDE.

A change in behavior with fly_deps is that modules come in scope only at their first reference. So, for example,

module A
let f = e
let g = B.h

the typeclass instances, SMT patterns etc. exported by B are not in scope for checking let f = e.

Another is that friend declarations must be the first declared dependence on a module. Otherwise, we report errors like this:

* Error 308 at /home/nswamy/workspace/everest/pulse/lib/core/PulseCore.Action.fsti(51,0-51,60):
  - Friend dependences must be declared as the first dependence on a module.
  - A non-friend dependence was already found on module
    PulseCore.InstantiatedSemantics.

--ext fly_deps is enabled throughout the F* repo, including in .fst.json config files for VS code. I expect it will become the default behavior at some point, but having it under a flag is to limit regressions in other repositories, until we all get a chance to use this feature and shake out any remaining issues.

…re; admitting a couple of proofs in X64.Vale.Decls that take ages, though they succeed
@nikswamy nikswamy marked this pull request as ready for review December 13, 2025 00:56
@nikswamy nikswamy changed the title refactoring dependence analysis to allow incremental analysis of decl… Loading dependences on the fly Dec 13, 2025
@nikswamy
Copy link
Collaborator Author

FYI, fly_deps also works in Karamel and in pulse (with some small changes to ordering for friend declarations)

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