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

ModuleSystem panic #1330

Closed
weaversa opened this issue Mar 1, 2022 · 1 comment · Fixed by #1331
Closed

ModuleSystem panic #1330

weaversa opened this issue Mar 1, 2022 · 1 comment · Fixed by #1331
Labels
bug Something not working correctly

Comments

@weaversa
Copy link
Collaborator

weaversa commented Mar 1, 2022

It seems that Cryptol panics if a file includes a file that imports a module.

$ more modA.cry
module modA where

x = 1
$ more include.cry 
import modA

y = 3
$ more main.cry 
include "include.cry"

z = 3
$ cryptol main.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.12.0.99
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Main
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  UNKNOWN
  Branch:    UNKNOWN
  Location:  ModuleSystem
  Message:   Interface not available
             modA
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.12.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/ModuleSystem/Monad.hs:475:18 in cryptol-2.12.0.99-inplace:Cryptol.ModuleSystem.Monad
%< --------------------------------------------------- 

@yav yav added the bug Something not working correctly label Mar 1, 2022
@yav
Copy link
Member

yav commented Mar 1, 2022

The issue here is that before loading a module, we need to load its dependencies. The problem arises because we are computing the dependencies from the parsed modules, but before includes are resolved, and as a result dependencies arising from included files are missed.

yav added a commit that referenced this issue Mar 2, 2022
We have to do that, so that we can see included imports, and thus load
the correct dependencies for a module.

This fixes #1330
@yav yav closed this as completed in #1331 Mar 3, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants