Search the scope of imported libraries #2701
Labels
scope
Issues relating to scope checking
type: enhancement
Issues and pull requests about possible improvements
ux: error reporting
Issues to do with how Agda reports errors
ux: library management
Issues relating to the library management system
Milestone
Comments
andreasabel
added
ux: error reporting
asr
added
the
type: enhancement
|
- [ ] Benchmark for memory consumption.
- [ ] Provide a verbosity switch that reports for each library some number that is at least closely connected with the memory occupied.
- [ ] Provide a command-line switch to turn it off, for cases where memory is tight anyways.
EDIT (Andreas): github does not render these check boxes, maybe it takes them only from one comment.
|
andreasabel
added a commit
that referenced
this issue
Aug 17, 2017
andreasabel
added a commit
that referenced
this issue
Aug 17, 2017
|
@WolframKahl : good points! We could cache a search index which is only rebuilt when a module of one of the used libraries changes. This would keep memory use pretty low, I suppose. |
andreasabel
added a commit
that referenced
this issue
Aug 18, 2017
andreasabel
added a commit
that referenced
this issue
Aug 19, 2017
|
We could even lazily build the search index only when it is used, i.e., by an error message or user query. For code that compiles in batch mode, this would be zero overhead then. The search index can be built from the .agdai files, even out-dated ones. Basically from the last compilable state. This is important because we need it in cases where there are scope errors. |
|
The search index can be built from the .agdai files, even out-dated ones. Basically from the last compilable state.
The last .agdai file still might contain completely different identifiers than the current source.
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Now that we have the
.agda-libfiles, we could use the libraries to improve theNotInScopeerror to also list hits in the non-imported files of the libraries in the project.Steps to make this work:
get all the source files of a library.
This could either be directory search, or we agree on a convention that if
Everything.agdaorREADME.agdaare present, then only this file is used (and recursively its imports). We could also add to the library description a "main" file which imports everything in the library.Deserialize only the scope of the interface files. This requires some skrewing with the import logic or the deserializer.
Keep the deserialized scopes in a separate
ScopeInfostructure, allowing ambiguities.Query this
ScopeInfofor names that are not in scope, or similar ones. We already have this functionality for the current scope.We might have to worry about a lot of false positives. Maybe for things from the libraries which are not in scope, we should only list exact matches.
Additionally, we could have an interactive command to search for identifiers in the libraries attached to the project. That would require almost no new work then.
The text was updated successfully, but these errors were encountered: