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

:prove, :check, and :exhaust error on out-of-scope import list exclusion #639

Closed
WeeknightMVP opened this issue Aug 15, 2019 · 1 comment
Labels
bug Something not working correctly command-line-repl Related to Cryptol's text-based UI cryptol-quickcheck Related to REPL :check command

Comments

@WeeknightMVP
Copy link

/* M.cry */
module M where
  f (a:Bit) = a
  property p a = f a == a
/* C.cry */
module C where
  import M (f)
$ cryptol C.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.7.1 (1e11ff6)

Loading module Cryptol
Loading module M
Loading module C
C> :check
property M::p 
[error] at <interactive>:1:1--1:5 Value not in scope: M::p
C> :exhaust
property M::p 
[error] at <interactive>:1:1--1:5 Value not in scope: M::p
C> :prove
:prove M::p
	
[error] at <interactive>:1:1--1:5 Value not in scope: M::p
@yav yav added cryptol-quickcheck Related to REPL :check command driver labels Jan 21, 2020
@yav yav added command-line-repl Related to Cryptol's text-based UI bug Something not working correctly and removed driver labels Sep 17, 2020
@yav
Copy link
Member

yav commented Sep 17, 2020

I believe the correct behavior here should be the commands check all properties that are in scope (either qualified or not). The current behavior is clearly wrong.

@robdockins robdockins mentioned this issue Dec 9, 2020
robdockins added a commit that referenced this issue Dec 10, 2020
the loaded properties.  Instead of listing all the loaded properties
and then parsing their names, we instead directly use the internal
names retrieved from the module.  This avoids problems arising from
the names of the properties not being in scope.

Separately, we should add settings for controlling exactly
which properties should be considered; right now it is always
all loaded properties.

Fixes #639
robdockins added a commit that referenced this issue Dec 10, 2020
robdockins added a commit that referenced this issue Dec 21, 2020
the loaded properties.  Instead of listing all the loaded properties
and then parsing their names, we instead directly use the internal
names retrieved from the module.  This avoids problems arising from
the names of the properties not being in scope.

Separately, we should add settings for controlling exactly
which properties should be considered; right now it is always
all loaded properties.

Fixes #639
robdockins added a commit that referenced this issue Dec 21, 2020
robdockins added a commit that referenced this issue Dec 21, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly command-line-repl Related to Cryptol's text-based UI cryptol-quickcheck Related to REPL :check command
Projects
None yet
Development

No branches or pull requests

2 participants