Update Satore README

PiperOrigin-RevId: 363137622
2026-05-28 19:31:14 +08:00 · 2021-03-16 09:27:07 +00:00
parent db5c562251
commit 25bd036e91
13 changed files with 30 additions and 49 deletions
@@ -6,7 +6,6 @@

 (require define2
         define2/define-wrapper
-         global
         racket/format
         racket/list
         racket/string
@@ -15,45 +15,51 @@ https://download.racket-lang.org
 Note for Linux users: Do read the comments on the download page.

 You may need to
-[configure the PATH environment variable](https://github.com/racket/racket/wiki/Set-your-PATH-environment-variable)
+[configure the PATH environment variable](https://github.com/racket/racket/wiki/Configure-Command-Line-for-Racket)
 to include the directory containing the `racket` and `raco` executables.

 To install **satore** and its dependencies (all are Apache2/MIT licensed),
-in a directory of your choice, type:
+type:

 ```shell
 raco pkg install --auto --update-deps satore
 ```
+
 <!--
-We use git clone instead of the git facility of `raco` so that
-the code is available at a location of the user's choice.
+Cloning only the correct subdirectory of the deemind-research repository is
+inconvenient, but the Racket package does that itself rather nicely.
 -->

 ## Running Satore

-Run a trivial example:
-
-```shell
-racket -l- satore -p satore/examples/socrates.p --proof
-```
-
-To see the various flags:
+First, you can check that satore is correctly installed by typing:

 ```shell
 racket -l- satore --help
 ```

-The .p file is assumed to be a standalone file with only comments and
+There are some examples in the `examples` subdirectory of the `satore`
+directory, and its location can be found with
+
+```shell
+racket -e '(displayln (collection-file-path "examples" "satore"))'
+```
+
+Run a trivial example:
+
+```shell
+racket -l- satore -p path-to-satore/examples/socrates.p --proof
+```
+
+The `.p` file is assumed to be a standalone file with only comments and
 `cnf(…).` lines without equality, where the logic clause must be surrounded by
 parentheses. All axioms must be included. (This will likely be improved soon.)

-Note that `racket -l- satore` can be invoked from anywhere.
-
 ## Results on TPTP 7.2.0 (corrected)

 Corrected results on TPTP 7.2.0, on a 2-2.5GHz CPU, with a limit of 5 minutes
 and 32GB per problem, either with the default settings, or with
-`--no-discover-online` to disable atom rewriting.
+`--no-discover-online` to disable atom rewriting:

 ```
 ┌────────────────────────────┬───────┬───────┬───────┬───────┬───────┬────────┐
@@ -10,7 +10,6 @@
         racket/format
         racket/list
         racket/pretty
-         satore/clause
         satore/tptp
         satore/unification
         text-table)
@@ -5,7 +5,6 @@
 ;***************************************************************************************;

 (require bazaar/cond-else
-         bazaar/debug
         bazaar/list
         bazaar/loop
         bazaar/mutation
@@ -13,14 +12,11 @@
         define2
         global
         racket/file
-         racket/format
         racket/list
-         racket/pretty
         satore/misc
         satore/trie
         satore/unification
-         syntax/parse/define
-         text-table)
+         syntax/parse/define)

 (provide (all-defined-out))

@@ -4,8 +4,7 @@
 ;****                                  Json Output                                  ****;
 ;***************************************************************************************;

-(require bazaar/debug
-         racket/dict
+(require racket/dict
         racket/string)

 (provide (all-defined-out))
@@ -4,16 +4,10 @@
 ;****                               Various Utilities                               ****;
 ;***************************************************************************************;

-(require (for-syntax racket/base racket/port racket/syntax syntax/parse)
-         (except-in bazaar/order atom<=>)
+(require (for-syntax racket/base racket/port racket/syntax)
         global
-         racket/contract
         racket/format
-         racket/list
-         racket/match
-         racket/port
-         racket/struct
-         racket/stxparam)
+         racket/port)

 (provide (all-defined-out))

@@ -1,8 +1,6 @@
 #lang racket/base

-(require global
-         racket/dict
-         racket/list
+(require racket/dict
         rackunit
         satore/clause
         satore/misc
@@ -1,17 +1,13 @@
 #lang racket/base

 (require (for-syntax racket/base syntax/parse)
-         bazaar/debug
         define2
-         define2/define-wrapper
         global
         racket/list
         racket/pretty
         rackunit
-         (submod satore/Clause test)
         satore/Clause
         satore/clause
-         satore/clause-format
         satore/rewrite-tree
         satore/unification)

@@ -4,7 +4,6 @@
         (except-in bazaar/order atom<=>)
         racket/file
         racket/list
-         racket/pretty
         racket/random
         rackunit
         (submod satore/Clause test)
@@ -1,6 +1,6 @@
 #lang racket/base

-(require (for-syntax racket/base syntax/parse)
+(require (for-syntax racket/base)
         define2
         define2/define-wrapper
         global
@@ -1,7 +1,6 @@
 #lang racket/base

-(require racket/pretty
-         rackunit
+(require rackunit
         satore/trie
         (only-in satore/unification symbol-variable?))

@@ -12,12 +12,9 @@
 ;;;   are lists of literals, and the same Clause can appear in different leaves
 ;;;   of the trie. Unification is only one of the operations performed on Clauses.

-(require bazaar/cond-else
-         bazaar/debug
-         bazaar/list
+(require bazaar/list
         bazaar/loop
         bazaar/mutation
-         (except-in bazaar/order atom<=>)
         define2
         global
         racket/list
@@ -18,8 +18,7 @@
         racket/dict
         racket/list
         racket/match
-         (submod racket/performance-hint begin-encourage-inline)
-         satore/misc)
+         (submod racket/performance-hint begin-encourage-inline))

 (provide (all-defined-out))