From ca871606c76fbc0995a870b4e6ff68c6aada1a4c Mon Sep 17 00:00:00 2001 From: Peter Lammich Date: Mon, 25 Mar 2024 15:15:26 +0100 Subject: [PATCH] upd links to 2023 --- docs/index.html | 9 +++++---- docs/index.md | 13 ++++++++----- index.in.md | 13 ++++++++----- index.md | 13 ++++++++----- 4 files changed, 29 insertions(+), 19 deletions(-) diff --git a/docs/index.html b/docs/index.html index b0f7f2f..2d84382 100644 --- a/docs/index.html +++ b/docs/index.html @@ -182,7 +182,7 @@

Getting Started

You can browse the theories or download the files. (The download link won’t work if you are browsing this from inside the downloaded archive!)

Warning: the .thy files in the download are best viewed with the Isabelle/HOL IDE.

Git Repository

-

The project is hosted on github github.com/lammich/isabelle_llvm/tree/2022

+

The project is hosted on github github.com/lammich/isabelle_llvm/tree/2023

Starting Points for Browsing

Here are some default starting points for browsing the theories

Parallel Paper

@@ -204,7 +204,8 @@

Verified Algorithms

PDQ Sort

Knuth Morris Pratt String Search

Binary Search

-

For the ISA-SAT verified SAT solver, see its own homepage

+

ISA-SAT verified SAT solver: homepage

+

lrat-isa UNSAT certificate checker: homepage

Isabelle-LLVM

IICF (Isabelle-LLVM + Refinement Framework + Collection Framework)

Shallow Embedding of LLVM Semantics

@@ -212,7 +213,7 @@

Prerequisites

Compiling and running benchmarks

@@ -223,7 +224,7 @@

Compiling and running benchmarks

cd sorting make run

This will run the binary search, KMP, and parallel sorting benchmarks. Warning: We have only tested this on a Linux x86_64 platform so far. We do not (yet) know how LLVM will digest our code on other platforms.

-

To render the benchmark results as pdf file, type (still in sorting directory):

+

To render the sorting benchmark results as pdf file, type (still in sorting directory):

make report

Re-Checking the Proofs

To re-check the proofs, run

diff --git a/docs/index.md b/docs/index.md index 96e4d55..61608e6 100644 --- a/docs/index.md +++ b/docs/index.md @@ -34,7 +34,7 @@ The main features are: Warning: the .thy files in the download are best viewed with the [Isabelle/HOL](https://isabelle.in.tum.de) IDE. ### Git Repository - The project is hosted on github [github.com/lammich/isabelle_llvm/tree/2022](https://github.com/lammich/isabelle_llvm/tree/2022) + The project is hosted on github [github.com/lammich/isabelle_llvm/tree/2023](https://github.com/lammich/isabelle_llvm/tree/2023) ### Starting Points for Browsing Here are some default starting points for browsing the theories @@ -82,8 +82,11 @@ The main features are: [Binary Search](browser_info/Unsorted/Examples/Bin_Search.html) - For the ISA-SAT verified SAT solver, see its own [homepage](https://m-fleury.github.io/isasat/isasat.html) - + ISA-SAT verified SAT solver: [homepage](https://m-fleury.github.io/isasat/isasat.html) + + lrat-isa UNSAT certificate checker: [homepage](https://github.com/lammich/lrat_isa) + + #### Isabelle-LLVM [IICF (Isabelle-LLVM + Refinement Framework + Collection Framework)](browser_info/Unsorted/Isabelle_LLVM/IICF.html) @@ -96,7 +99,7 @@ The main features are: * To re-check the proofs: Working installation of [Isabelle/HOL](https://isabelle.in.tum.de) with the [Archive of Formal Proofs](https://www.isa-afp.org) installed as as described on [https://www.isa-afp.org/using.shtml](https://www.isa-afp.org/using.shtml). - We require version = Isabelle-2022, which, at the time of writing, is the current version. + We require version = Isabelle-2023, which, at the time of writing, is the current version. * To run the regression tests: [Valgrind](https://www.valgrind.org/) version >= 3.0.0 ## Compiling and running benchmarks @@ -112,7 +115,7 @@ The main features are: Warning: We have only tested this on a Linux x86_64 platform so far. We do not (yet) know how LLVM will digest our code on other platforms. - To render the benchmark results as pdf file, type (still in sorting directory): + To render the sorting benchmark results as pdf file, type (still in sorting directory): make report diff --git a/index.in.md b/index.in.md index aa9bde0..07647c8 100644 --- a/index.in.md +++ b/index.in.md @@ -34,7 +34,7 @@ The main features are: Warning: the .thy files in the download are best viewed with the [Isabelle/HOL](https://isabelle.in.tum.de) IDE. ### Git Repository - The project is hosted on github [github.com/lammich/isabelle_llvm/tree/2022](https://github.com/lammich/isabelle_llvm/tree/2022) + The project is hosted on github [github.com/lammich/isabelle_llvm/tree/2023](https://github.com/lammich/isabelle_llvm/tree/2023) ### Starting Points for Browsing Here are some default starting points for browsing the theories @@ -82,8 +82,11 @@ The main features are: [Binary Search](:Examples:/Bin_Search.html) - For the ISA-SAT verified SAT solver, see its own [homepage](https://m-fleury.github.io/isasat/isasat.html) - + ISA-SAT verified SAT solver: [homepage](https://m-fleury.github.io/isasat/isasat.html) + + lrat-isa UNSAT certificate checker: [homepage](https://github.com/lammich/lrat_isa) + + #### Isabelle-LLVM [IICF (Isabelle-LLVM + Refinement Framework + Collection Framework)](:Isabelle_LLVM:/IICF.html) @@ -96,7 +99,7 @@ The main features are: * To re-check the proofs: Working installation of [Isabelle/HOL](https://isabelle.in.tum.de) with the [Archive of Formal Proofs](https://www.isa-afp.org) installed as as described on [https://www.isa-afp.org/using.shtml](https://www.isa-afp.org/using.shtml). - We require version = Isabelle-2022, which, at the time of writing, is the current version. + We require version = Isabelle-2023, which, at the time of writing, is the current version. * To run the regression tests: [Valgrind](https://www.valgrind.org/) version >= 3.0.0 ## Compiling and running benchmarks @@ -112,7 +115,7 @@ The main features are: Warning: We have only tested this on a Linux x86_64 platform so far. We do not (yet) know how LLVM will digest our code on other platforms. - To render the benchmark results as pdf file, type (still in sorting directory): + To render the sorting benchmark results as pdf file, type (still in sorting directory): make report diff --git a/index.md b/index.md index 96e4d55..61608e6 100644 --- a/index.md +++ b/index.md @@ -34,7 +34,7 @@ The main features are: Warning: the .thy files in the download are best viewed with the [Isabelle/HOL](https://isabelle.in.tum.de) IDE. ### Git Repository - The project is hosted on github [github.com/lammich/isabelle_llvm/tree/2022](https://github.com/lammich/isabelle_llvm/tree/2022) + The project is hosted on github [github.com/lammich/isabelle_llvm/tree/2023](https://github.com/lammich/isabelle_llvm/tree/2023) ### Starting Points for Browsing Here are some default starting points for browsing the theories @@ -82,8 +82,11 @@ The main features are: [Binary Search](browser_info/Unsorted/Examples/Bin_Search.html) - For the ISA-SAT verified SAT solver, see its own [homepage](https://m-fleury.github.io/isasat/isasat.html) - + ISA-SAT verified SAT solver: [homepage](https://m-fleury.github.io/isasat/isasat.html) + + lrat-isa UNSAT certificate checker: [homepage](https://github.com/lammich/lrat_isa) + + #### Isabelle-LLVM [IICF (Isabelle-LLVM + Refinement Framework + Collection Framework)](browser_info/Unsorted/Isabelle_LLVM/IICF.html) @@ -96,7 +99,7 @@ The main features are: * To re-check the proofs: Working installation of [Isabelle/HOL](https://isabelle.in.tum.de) with the [Archive of Formal Proofs](https://www.isa-afp.org) installed as as described on [https://www.isa-afp.org/using.shtml](https://www.isa-afp.org/using.shtml). - We require version = Isabelle-2022, which, at the time of writing, is the current version. + We require version = Isabelle-2023, which, at the time of writing, is the current version. * To run the regression tests: [Valgrind](https://www.valgrind.org/) version >= 3.0.0 ## Compiling and running benchmarks @@ -112,7 +115,7 @@ The main features are: Warning: We have only tested this on a Linux x86_64 platform so far. We do not (yet) know how LLVM will digest our code on other platforms. - To render the benchmark results as pdf file, type (still in sorting directory): + To render the sorting benchmark results as pdf file, type (still in sorting directory): make report