Lurch Options

We just use a global for storing the current options. This avoids having to pass it as an optional argument through the entire validation chain of interpretations and validation tools. To set an option just do e.g. LurchOptions.avoidLoneMetavars = false. Current validation options are:

• validateall - if true, validate all inferences. If false, only validate the target.
• checkPreemies - Check for preemies iff this is true
• processBIHs - process BIHs iff this is true
• instantiateEverything - don't avoid anything below (equivalent to setting the next three settings to false)
• avoidLoneMetavars - if true don't try to instantiate lone metavariables, otherwise try to instantiate them with every user proposition.
• avoidLoneEFAs - the same thing for lone EFAs
• avoidLoneElementOfs - the same thing for lone x∈A's where A is a metavariable
• processChains - process chains and equations iff this is true
• processEquations - process equations iff this is true
• processCases- process the cases tool iff this is true
• autoCases - similar to avoidLoneMetavars=false. If true, then identify all Cases-like rules and try to instantiate their univar conclusion with every user's conclusion in the document.
• processCAS - process CAS tool iff this is true
• processAlgebra - use the CAS tool to validate equations followed by 'by algebra' iff this is true
• swapTheoremProofPairs - move theorems after their next sibling if its a proof
• updateProgress - the function that gives progress updates while instantiating
• updateFreq - how often to give a progress update during a pass
• badResultMsg - what the feedback message should be internally to expressions which are not found to be propositionally valid
• runStudentTests - use all of the student test files in the acid test suite
• startStudentTest - the number of the first student test to run
• endStudentTest - the number of the last student test to run

Create a document index, add it to the document, and populate it. The second argument specifies the type of index to make. The types correspond to the various phases of processing.

addLurchIndices

This routine populates the generic tree indexer with the index definition we need for a Lurch document. It will usually be called by the addIndex(doc) routine to create, define, and populate a document's index which can then be accessed via doc.index.

A JSON stringification that is predictable. The standard JSON.stringify() can produce different outputs unpredictably, because there is no required ordering on the key-value pairs. This one requires keys to be output in increasing string order, so it is predictable.