nasalib.all

# Ordered list of libraries to be processed by proveit. Each line in <file> has the form
# <lib> [: <options>], where <lib> is a directory name and <options>
# are paramters to proveit. If <lib> is empty, options apply to
# all libraries thenceforth.
: --log --disable-oracles --dir summaries # Save summary files in summaries/
: --summary-mode md
ints
structures
reals
orders
analysis
sets_aux
numbers
series
trig
vectors
sigma_set        
algebra
vect_analysis
lnexp
power
interval_arith
affine_arith 
matrices
Bernstein
Sturm
Tarski
MetiTarski  : --enable metit
fast_approx : --enable metit
shapes      : --enable metit
complex
digraphs         
fault_tolerance
float/float_bounded_axiomatic
float/float_bounded
float/float_unbounded
float/float_ieee854
graphs             
pvsio_utils
pvsio_utils/PVSioChecker
pvsio_utils/PVSioCSV
pvsio_utils/PVSioKeyVal
LTL
exact_real_arith 
aviation : --enable metit
ACCoRD : --enable metit
sorting          
nominal
TRS              
CCG
PVS0  
Riemann 
topology            
complex_alt         
scott               
while               
extended_nnreal     
metric_space        
measure_integration 
complex_integration 
lebesgue            
probability         
co_structures       
TU_Games            
linear_algebra      
ASP                 
line_segments       
polygons            
polygon_merge       
mv_analysis
ODEs
dL
mult_poly
## Examples
examples : --enable metit -sf 
algebra/algebra_examples
pvsio_utils/pvsio_examples
# dL/dL_examples : --enable metit
# dL/dL_RTA: --enable metit
# dL/dL_LTL_examples: --enable metit
# dL/dL_Liveness_examples : --enable metit
## Deprecated libraries
# decimals         # Included in PVSio since 7.0
# lnexp_fnd        # Renamed lnexp since 7.0
# trig_fnd         # Replaced by trig 
# groups           # Merged into the algebra library