8000 --ignore-interfaces should not ignore builtin modules nor libraries depended on · Issue #2754 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content
--ignore-interfaces should not ignore builtin modules nor libraries depended on #2754
New issue
New issue
Open
Open
--ignore-interfaces should not ignore builtin modules nor libraries depended on#2754
Labels
builtinEnhancements to the builtin modules and builtin definitionsimportIssues to do with importing modulesinterfaceSerialization and loading of interface fileslevelstype: enhancementIssues and pull requests about possible improvementsux: library managementIssues relating to the library management system
Milestone
 
icebox
@nad

Description

@nad
nad
opened on Sep 13, 2017

The following code (an empty file) triggers an internal error if -vtc:10 --ignore-interfaces is used:



Output:


[...]
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Level.hs:77

Metadata
Metadata
Assignees
No one assigned
    Labels
    builtinEnhancements to the builtin modules and builtin definitionsimportIssues to do with importing modulesinterfaceSerialization and loading of interface fileslevelstype: enhancementIssues and pull requests about possible improvementsux: library managementIssues relating to the library management system
    Type
    No type
    Projects
    No projects
    Milestone
    Relationships
    None yet
    Development
    No branches or pull requests
    Issue actions
      
      



  



  
      

      

    
      
  
      

  
      

          



    



  

    

    

    





    
      
    
      
    
      
  



0