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

Parameterized modules in the REPL #998

Closed
ghost opened this issue Dec 8, 2020 · 4 comments
Closed

Parameterized modules in the REPL #998

ghost opened this issue Dec 8, 2020 · 4 comments
Labels
parameterized modules Related to Cryptol's parameterized modules

Comments

@ghost
Copy link

ghost commented Dec 8, 2020

How can I interact with a parameterized module when it is loaded in the REPL?

I usually make a second, single line module that "backtick" imports the parameterized one, but I saw in #815 that this is up for removal. It got me wondering if there is (or will be) a way that I can set and change parameters from within the REPL when such a module is loaded.

@robdockins robdockins added the parameterized modules Related to Cryptol's parameterized modules label Dec 9, 2020
@robdockins
Copy link
Contributor

We're still in the design phase on the new module system, so things are a bit fluid. Let me see if I understand the use case you are concerned about. You'd like to be able to load a parameterized module at the REPL by setting the parameters directly from the prompt; is that right?

@ghost
Copy link
Author

ghost commented Dec 11, 2020

Right. At the REPL, I'd like some way to use the definitions from a parameterized module without needing to make a new file for a specific instantiation or for a "backtick" import like I do now. Otherwise why can I load parameterized modules at all?

I originally intended to ask if a parameterized module could behave as if it was "backtick" imported when loaded with :l, but then I saw the redesign post. If those imports are removed, maybe :l could accept additional arguments for setting parameters from the prompt.

@yav
Copy link
Member

yav commented Dec 11, 2020

Loading an uninstantiated parameterized module is quite useful, for example:

  1. to check that module loads during development, or
  2. so you can browse the contents of a module
    So we'll likely continue to support loading uninstantiated modules.

The new design is not yet solidified, but one of our goals is to make it more convenient to instantiate parameterized modules, so perhaps this would be less of an issue, but we could still consider some mechanism for setting parameters on the REPL.

@yav
Copy link
Member

yav commented Feb 19, 2025

The backick modules did end up staying in the design, so I'll close this for now.

@yav yav closed this as completed Feb 19, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
parameterized modules Related to Cryptol's parameterized modules
Projects
None yet
Development

No branches or pull requests

2 participants