dag-tools's People
dag-tools's Issues
Parse literal names to check dependencies
Many tactics include names of variables as part of their code, for instance they apply some lemma by name like `eq.symm�
.
The declarations these names refer to often need to be available at elaboration time of the tactic (unless the ```(blah)
syntax is used).
We can detect these dependencies by taking expressions like name.of_string
and turning them into actual names of dependencies
Make the import optimizer not use dep counts
I think we are really only computing reachable sets in the end, dep counts will be useful for file splits still, but the logic of import optimizer can be simplified
Add some actual tests
Allow recursive removal
When recommending removal of imports we should update the dag and print a sed script that fixes later imports too.
This is possibly incompatible with working asynchronously!
Add a robust mode
This should never fail and be extremely pessimistic / cautious, i.e. if a file contains and decl of type tactic don't remove it.
Also don't recommend any file whose imports go to zero or any files containing a _localized.blah
Finish updating other dag operators to use dfs
use run_simple instead of manually matching the tactic state
Parse names in tactic
One common false positive is when a tactic uses a lemma by name, this wont be parsed as an unecessary import right now but we should convert terms representing names of lemmas in to the names and add those dependencies.
Switch to using module_info as an alternative backend
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.