-
Notifications
You must be signed in to change notification settings - Fork 50
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
Removing unused files, dead code. #157
Comments
What about the whole API folder? There is also some mysterious looking ProofSimplifier in Shell. |
Very possibly @quickbeam123! I'm going to chat with Giles Monday about any politics I need to be aware of, then start deleting things in order of least-likely-to-be-wanted first. |
Inferences/InterpretedSimplifier is completed commented out. Perhaps it can be removed. |
Some values in TimeCounterUnit most likely don't occur in the code anymore... Like TC_BDD_CLAUSIFICATION, etc. Could be removed as well! |
There also some code, authored by Ioan, generally guarded by |
Got another one: CTFwSubsAndRes.*
So, transitively, CodeTreeSubsumptionIndex is also unused and maybe some other indices are formally alive but unused because of how IndexManager works. |
@quickbeam123 - good spot, I think @JakobR plans to fix something in this region - perhaps they can comment to see what they need? |
@MichaelRawson feel free to remove CTFwSubsAndRes; I will revive it from the history in case I need it later. It would be nice if we could keep |
@JakobR - thanks. OK, CTFw can go but I'll keep code trees - I'm not in a hurry to delete stuff people want, only the stuff nobody wants. :-) |
@easychair and/or @quickbeam123 - a reminder, do you have some data about which options are/are not useful in terms of schedules? Naturally it's not the only consideration when removing something, but it's a pretty good indicator. |
I have lot's of data, but it's not so easy to interpret it. Most notably, it's not entirely clear where draw the line and call an option/value not worth maintaining. For most of the cases, one can find a problem that the database cannot solve otherwise... (then how many lost solution can be reclaimed by more search, or how many lost solutions are worth sacrificing for better maintenance?) |
I think this is the crux of it. Maybe we can start by ranking options in terms of effectiveness? Is that a reasonable thing to do? |
Some code in Vampire's tree appears to no longer be used. While this is not a problem in itself, it adds to the noise for new contributors and some dead code is still being compiled or even linked (see e.g. PR #153 to remove Lingeling sources). Additionally, changes to interfaces require more effort as code that is no longer used needs fixing.
After some discussion with others, I believe some of the following could be removed:
Saturation/Limits
are empty files.Shell/SimplifyProver
isn't used anywhere - used to be support for the Simplify theorem prover's languageShell/ProofSimplifier
BFNT
andBFNTMainLoop
is an old form of finite model building.Inferences/InterpretedSimplifier
commented outIndexing/ArithmeticIndex
commented outVUtil
and friends - no longer build, not touched in several yearsvutil
ucompit
vclausify
vcompit
vground
vsat
vltb
vtest
Test
TimeCounterUnit
:TC_BDD
etc.TWLSolver
Lib::InPlaceStack
Lib::Graph
MatchTag
OptionsReader
FormulaIndex
CTFwSubsAndRes
CParser
EqualityAxiomatiser
GlobalOptions
Refutation
PDUtils
#if GNUMP
SAT::Preprocess
Inferences::SLQueryForwardSubsumption
,Inferences::RefutationSeekerFSE
EGSubstitution
Kernel/RobSubstitution
Kernel/SortHelper
Kernel/Currifier.hpp
Term::askDistinctVars
Lib::LastCopyWatcher
Inferences::HyperSuperposition
PortfolioMode::waitForChildAndCheckIfProofFound
Formula.cpp
DECLARE_PLACEMENT_NEW
TermSharing::insertRecurrently
Lib::TimeCounter
Shell::Profile
FoolAwareSubformulaIterator
andFoolAwareSubtermIterator
InstGen
ArrayTheoryISE
Api/
env.out()
Lib::MemoryLeak
Matcher
:OCMatchIterator
,MatchIterator
...limitMemory
, we control its allocations.Lib::MultiCounter
applyToLiteral
inSubstHelper
scripts
seem like they might no longer serve a purpose.SortHelper::getTermSort
Some things might be used in the near future, but currently are not.
CodeTreeSubsumptionIndex
andClauseCodeTree
, orphaned byCTFwSubsAndRes
- see below.Credit to @quickbeam123, @ibnyusuf and @selig for identifying some of these. What I'd like from the team is help to identify more unused files or dead code, as well as rescuing files that need to be kept.
Eventually things that are still on the list will be removed by PR. Fear not, however, one of the many virtues of source control is the ability to reanimate code from beyond the grave. Thank you!
The text was updated successfully, but these errors were encountered: