Update README.md

Author: dnezam

candle/set-theory/README.md

@@ -13,6 +13,3 @@ Specification of (roughly) Zermelo's set theory.
 Two main definitions:
   is_set_theory (mem : 'U -> 'U -> bool), and
   is_model (mem, indset, ch)
-
-[zfc](zfc):
-An old formalisation of set theory

compiler/backend/README.md

@@ -17,9 +17,6 @@ This directory contains the ARMv8-specific part of the compiler backend.
 This directory contains proofs for the ASL-derived ARMv8-specific part of the
 compiler backend.
 
-[backendComputeLib.sml](backendComputeLib.sml):
-A compset for evaluating the compiler backend inside the logic of HOL.
-
 [backendScript.sml](backendScript.sml):
 Composes all of the compiler phases within the compiler backend into
 a single compile function which is connected (in ../compilerScript.sml)

compiler/backend/ag32/README.md

@@ -1,9 +1,6 @@
 This directory contains the Silver-specific part of the compiler
 backend and associated proofs.
 
-[ag32_compileLib.sml](ag32_compileLib.sml):
-Provides a compset for the ag32-specific parts of the backend
-
 [ag32_configScript.sml](ag32_configScript.sml):
 Define the compiler configuration for ag32
 

compiler/backend/arm7/README.md

@@ -1,8 +1,5 @@
 This directory contains the ARMv7-specific part of the compiler backend.
 
-[arm7_compileLib.sml](arm7_compileLib.sml):
-Provides a compset for the ARMv7-specific parts of the backend
-
 [arm7_configScript.sml](arm7_configScript.sml):
 Define the compiler configuration for ARMv7
 

compiler/backend/arm8/README.md

@@ -1,8 +1,5 @@
 This directory contains the ARMv8-specific part of the compiler backend.
 
-[arm8_compileLib.sml](arm8_compileLib.sml):
-Provides a compset for the ARMv8-specific parts of the backend
-
 [arm8_configScript.sml](arm8_configScript.sml):
 Define the compiler configuration for ARMv8
 

compiler/backend/mips/README.md

@@ -3,9 +3,6 @@ This directory contains the mips-specific part of the compiler backend.
 [export_mipsScript.sml](export_mipsScript.sml):
 Define the format of the compiler-generated .S file for MIPS
 
-[mips_compileLib.sml](mips_compileLib.sml):
-Provides a compset for the MIPS-specific parts of the backend
-
 [mips_configScript.sml](mips_configScript.sml):
 Define the compiler configuration for MIPS
 

compiler/backend/riscv/README.md

@@ -6,8 +6,5 @@ Define the format of the compiler-generated .S file for RISC-V
 [proofs](proofs):
 This directory contains the RISC-V-specific proofs.
 
-[riscv_compileLib.sml](riscv_compileLib.sml):
-Provides an eval for the RISC-V-specific parts of the backend
-
 [riscv_configScript.sml](riscv_configScript.sml):
 Define the compiler configuration for RISC-V

compiler/backend/x64/README.md

@@ -6,8 +6,5 @@ Define the format of the compiler-generated .S file for x64
 [proofs](proofs):
 This directory contains the x64-specific proofs.
 
-[x64_compileLib.sml](x64_compileLib.sml):
-Provides an eval for the x64-specific parts of the backend
-
 [x64_configScript.sml](x64_configScript.sml):
 Define the compiler configuration for x64

examples/README.md

@@ -6,18 +6,12 @@ found in their own top-level directories.
 [array_searchProgScript.sml](array_searchProgScript.sml):
 An example based on searching an array.
 
-[bot](bot):
-Formalization of the FFI and proofs for the VeriPhy pipeline.
-
 [catProgScript.sml](catProgScript.sml):
 cat program example: concatenate and print lines from files.
 
 [compilation](compilation):
 Compilation of the CakeML examples to different architectures.
 
-[cost](cost):
-Preliminary data-cost examples
-
 [deflate](deflate):
 Scripts relevant to the formalisation of the DEFLATE algorithm
 
@@ -36,10 +30,6 @@ Examples on the topic of doubling a number.
 [echoProgScript.sml](echoProgScript.sml):
 echo program example: print the command line arguments.
 
-[eval](eval):
-A simple example of using eval, to help work out the development of the
-bootstrapped compiler supporting eval.
-
 [filterProgScript.sml](filterProgScript.sml):
 Filter case study from CASE.
 

examples/opentheory/README.md

@@ -4,10 +4,6 @@ Implementation of an OpenTheory reader based on the Candle kernel.
 This directory contains the script that does in-logic compilation of
 the OpenTheory article checker.
 
-[monadIO](monadIO):
-This directory contains a version of the OpenTheory article checker
-where the I/O part is built using the monadic translator.
-
 [prettyScript.sml](prettyScript.sml):
 A pretty printer producing mlstring app_lists.
 Based on the pretty printer from "ML from the working programmer".

pancake/README.md

@@ -17,9 +17,6 @@ Simplification of arithmetic in crepLang.
 [crep_to_loopScript.sml](crep_to_loopScript.sml):
 Compilation from crepLang to panLang.
 
-[examples](examples):
-A few examples of timeLang programs
-
 [ffi](ffi):
 FFI for Pancake
 

pancake/proofs/README.md

@@ -33,6 +33,3 @@ composing semantics correctness from pan to target
 
 [pan_to_wordProofScript.sml](pan_to_wordProofScript.sml):
 Correctness proof for combined pan_to_word compilation.
-
-[time](time):
-Proof files for compiling TimeLang.