vprover · MichaelRawson · Mar 15, 2024
diff --git a/README.md b/README.md
@@ -1,18 +1,5 @@
-# vprover.github.io
-The Vampire project has a [website](https://vprover.github.io)!
+# Website
+The website is mostly retired now and points to the wiki instead.
+The hope is that this presents less of a barrier to entry for potential contributors.
 
-The website is hosted on GitHub pages, making some use of the Jekyll templating library.
-Generally stuff is obvious: copy the style of whatever is there already, it's hard to break.
-
-# New Members
-It's nice to have you on the [team page](https://vprover.github.io/team.html)!
-This is a simple process:
- - put a photo of yourself in `img/`: preferably a thumbnail, square aspect works best
- - add your name to `_includes/authors.html` - this allows you to have a short-form name and a hyperlink to your personal page if you like
- - add a section in `team.html` with a little about you and what you're doing - use the existing people's sections as inspiration
-
-Push to master directly, we don't care that much. Welcome!
-
-# News
-Add a news item by copying a file in `_posts` and updating the file name and fields accordingly.
-The list of news items will be updated automatically.
+If for some reason you need to fix something, it may be helpful to know that this was a 2017-era design using <a href="https://jekyllrb.com/docs/github-pages/">Jekyll and GitHub Pages</a>.
diff --git a/_includes/navigation.html b/_includes/navigation.html
@@ -4,14 +4,6 @@
   <i class="material-icons">menu</i>
  </label>
  <a href="/index.html">Vampire</a>
- <a href="/news.html">News</a>
  <a href="/download.html">Download</a>
- <a href="/licence.html">Licence</a>
- <a href="/usage.html">Usage</a>
  <a href="/team.html">Team</a>
- <a href="/pubs.html">Publications</a>
- <a href="/history.html">History</a>
- <a href="/trophies.html">Trophies</a>
- <a href="/projects.html">Projects</a>
- <a href="/workshop.html">Workshop</a>
 </nav>
diff --git a/_layouts/news.html b/_layouts/news.html
diff --git a/_posts/2017-11-01-revamp.md b/_posts/2017-11-01-revamp.md
diff --git a/_posts/2017-12-05-vampire-source-available.md b/_posts/2017-12-05-vampire-source-available.md
diff --git a/_posts/2017-12-10-vampire-mailing-list.md b/_posts/2017-12-10-vampire-mailing-list.md
diff --git a/_sass/pubs.scss b/_sass/pubs.scss
diff --git a/bin/vampire4.2.2 b/bin/vampire4.2.2
diff --git a/bin/vampire4.2.2_noz3 b/bin/vampire4.2.2_noz3
diff --git a/bin/vampire4.5_precasc b/bin/vampire4.5_precasc
diff --git a/bin/vampire4.5_precasc_thf b/bin/vampire4.5_precasc_thf
diff --git a/bin/vampire_rel_static_release_v4.4 b/bin/vampire_rel_static_release_v4.4
diff --git a/bin/vampire_z3_rel_static_release_v4.4 b/bin/vampire_z3_rel_static_release_v4.4
diff --git a/history.html b/history.html
diff --git a/index.html b/index.html
@@ -4,30 +4,23 @@
 ---
 
 <p>
-Automatic theorem proving has a number of important applications, such as software verification, hardware verification, 
-  hardware design, knowledge representation and reasoning, the Semantic Web, algebra, and proving theorems in mathematics. 
-Over 50 years of research in theorem proving have resulted in one of the most advanced and elegant theories in 
-  computer science.
-This area is an ideal target for scientific engineering: implementation techniques have to be developed to realise 
-  an advanced theory in practically valuable tools.
+Automatic theorem proving has a number of important applications, such as software verification, hardware verification, hardware design, knowledge representation and reasoning, the Semantic Web, algebra, and proving theorems in mathematics.
+Over 50 years of research in theorem proving have resulted in one of the most advanced and elegant theories in computer science.
+This area is an ideal target for scientific engineering: implementation techniques have to be developed to realise an advanced theory in practically valuable tools.
 </p>
 
 <p>
-Vampire is a theorem prover, that is, a system able to prove theorems &mdash; although now it can do much more! 
-Its main focus is in proving theorems in first-order logic but it can also prove non-theorems and build finite models, as well as reasoning in combinations of <em>theories</em>, such as arithmetic, arrays, and datatypes, and with higher-order logic. 
-The development of Vampire began in 1994 and has survived a number of rewritings (see <a href="https://vprover.github.io/history.html">history</a>). 
-</p>
-
-<p><b>NEW LICENCE!</b> We are very pleased to announce that Vampire is now available under a <a href="https://vprover.github.io/licence.html">BSD 3-Clause licence</a>, allowing (free) industrial and academic usage. 
-  It would be great to hear from you if you are making use of this new licence within your work. Please join our <a href="https://groups.google.com/g/vprover?pli=1"> very low-traffic mailing list</a> for updates. 
-You may also want to want to use the <a href="https://github.com/vprover/vampire/issues">GitHub Issues</a> page for questions or issues.
+<a href="https://github.com/vprover/vampire">Vampire</a> is a theorem prover, that is, a system able to prove theorems &mdash; although now it can do much more!
+Its main focus is in proving theorems in first-order logic but it can also prove non-theorems and build finite models, as well as reasoning in combinations of <em>theories</em>, such as arithmetic, arrays, and datatypes, and with higher-order logic.
+The development of Vampire began in 1994 and has survived a number of rewrites (see <a href="https://github.com/vprover/vampire/wiki/History">history</a>).
+Vampire is available under a modified BSD 3-clause licence (see the LICENCE), allowing (free) industrial and academic use.
 </p>
 
 <h3>Features</h3>
 <ul>
-  <li>Vampire is very fast, as can be judged by <a href="/trophies.html">our awards</a> at the CASC and SMT-COMP comeptitions</li>
-  <li>Vampire has an easy to use <i>portfolio mode</i> (see <a href="https://vprover.github.io/usage.html">Usage</a>) that can be run in multicore mode</li>
-  <li>Vampire can "pretend to be an SMT solver" in the sense that it accepts SMT-LIB input (see <a href="https://vprover.github.io/usage.html">Usage</a>)  and can effectively reason in combinations of first-order logic and theories, such as integer arithmetic, which makes it useful for reasoning with theories and quantifiers</li>
+  <li>Vampire is very fast, as can be judged by <a href="https://github.com/vprover/vampire/wiki/Trophies">our awards</a> at the CASC and SMT-COMP comeptitions</li>
+  <li>Vampire has an easy to use <em>portfolio mode</em> (see the README) that can be run in multicore mode</li>
+  <li>Vampire can "pretend to be an SMT solver" in the sense that it accepts SMT-LIB input and can effectively reason in combinations of first-order logic and theories, such as integer arithmetic, which makes it useful for reasoning with theories and quantifiers</li>
   <li>Vampire can produce detailed proofs and finite models</li>
   <li>Vampire supports (inductive) reasoning over algebraic data types (finite term algebras)</li>
   <li>Vampire can generate interpolants</li>

diff --git a/licence.html b/licence.html
diff --git a/license.html b/license.html
diff --git a/news.html b/news.html
diff --git a/projects.html b/projects.html