Update archive.

isabelle-prover · Feb 10, 2024 · ee6b9d4 · ee6b9d4
commit ee6b9d4
Show file tree

Hide file tree

Showing 20,183 changed files with 1,283,619 additions and 0 deletions.
diff --git a/.github/workflows/main.yaml b/.github/workflows/main.yaml
@@ -0,0 +1,20 @@
+on:
+  schedule:
+   - cron: '0 */4 * * *'
+
+jobs:
+  publish_archive_job:
+    runs-on: ubuntu-latest
+    name: A job to publish zulip-archive in GitHub pages
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v3
+    - name: Run archive
+      id: archive
+      uses: zulip/zulip-archive@master
+      with:
+        zulip_organization_url: ${{ secrets.zulip_organization_url }}
+        zulip_bot_email: ${{ secrets.zulip_bot_email }}
+        zulip_bot_key: ${{ secrets.zulip_bot_key }}
+        github_token: ${{ secrets.GITHUB_TOKEN }}
+        delete_history: true
diff --git a/.nojekyll b/.nojekyll
diff --git a/assets/img/zulip.svg b/assets/img/zulip.svg
diff --git a/index.html b/index.html
@@ -0,0 +1,42 @@
+<html>
+<head><meta charset="utf-8"><title>Zulip Chat Archive</title></head>
+<hr>
+
+<h2>Streams:</h2>
+
+<ul>
+<li> <a href="stream/336180-Archive-Mirror.3A-Isabelle-Users-Mailing-List/index.html">Archive Mirror: Isabelle Users Mailing List</a> (6817 topics) </li>
+
+<li> <a href="stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/index.html">Mirror: Isabelle Users Mailing List</a> (1427 topics) </li>
+
+<li> <a href="stream/238552-Beginner-Questions/index.html">Beginner Questions</a> (664 topics) </li>
+
+<li> <a href="stream/202961-General/index.html">General</a> (267 topics) </li>
+
+<li> <a href="stream/247542-Mirror.3A-Isabelle-Development-Mailing-List/index.html">Mirror: Isabelle Development Mailing List</a> (186 topics) </li>
+
+<li> <a href="stream/211483-Isabelle.2FML/index.html">Isabelle/ML</a> (64 topics) </li>
+
+<li> <a href="stream/214136-Announcements/index.html">Announcements</a> (29 topics) </li>
+
+<li> <a href="stream/202968-quantum-computing/index.html">quantum computing</a> (22 topics) </li>
+
+<li> <a href="stream/285459-Is-there-code-for-X.3F/index.html">Is there code for X?</a> (20 topics) </li>
+
+<li> <a href="stream/202967-New-Members-.26-Projects/index.html">New Members &amp; Projects</a> (15 topics) </li>
+
+<li> <a href="stream/245944-Proof-Ground/index.html">Proof Ground</a> (7 topics) </li>
+
+<li> <a href="stream/285806-SErAPIS/index.html">SErAPIS</a> (6 topics) </li>
+
+<li> <a href="stream/203204-Machine-Learning-for-Isabelle/index.html">Machine Learning for Isabelle</a> (5 topics) </li>
+
+<li> <a href="stream/211306-Lie/index.html">Lie</a> (3 topics) </li>
+
+<li> <a href="stream/282466-IRC-.23isabelle/index.html">IRC #isabelle</a> (2 topics) </li>
+
+<li> <a href="stream/336168-EMail-Test/index.html">EMail Test</a> (1 topic) </li>
+</ul>
+
+<hr><p>Last updated: Feb 10 2024 at 01:01 UTC</p>
+</html>
diff --git a/sitemap-001-pages.xml.gz b/sitemap-001-pages.xml.gz
diff --git a/sitemap.xml b/sitemap.xml
@@ -0,0 +1,6 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<sitemapindex xmlns="http://www.sitemaps.org/schemas/sitemap/0.9">
+	<!-- Powered by https://github.com/pigs-will-fly/py-xml-sitemap-writer -->
+	<!-- 1128 urls -->
+	<sitemap><loc>http://isabelle.systems/zulip-archive/sitemap-001-pages.xml.gz</loc></sitemap>
+</sitemapindex>
diff --git a/stream/202961-General/index.html b/stream/202961-General/index.html
diff --git a/stream/202961-General/topic/(no.20topic).html b/stream/202961-General/topic/(no.20topic).html
@@ -0,0 +1,19 @@
+<html>
+<head><meta charset="utf-8"><title>(no topic) · General · Zulip Chat Archive</title></head>
+<h2>Stream: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/index.html">General</a></h2>
+<h3>Topic: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/(no.20topic).html">(no topic)</a></h3>
+
+<hr>
+
+<base href="https://isabelle.zulipchat.com/">
+
+<head><link href="http://isabelle.systems/zulip-archive/style.css" rel="stylesheet"></head>
+
+<a name="262744558"></a>
+<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%28no%20topic%29/near/262744558" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Simon Wimmer <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/(no.20topic).html#262744558">(Nov 25 2021 at 22:21)</a>:</h4>
+<p>Ah nice! I'll ask him about it.</p>
+
+
+
+<hr><p>Last updated: Jul 15 2022 at 23:21 UTC</p>
+</html>
diff --git a/...m/202961-General/topic/.22Real.22.20imperative.20code.20generation.20from.20Isabelle.html b/...m/202961-General/topic/.22Real.22.20imperative.20code.20generation.20from.20Isabelle.html
diff --git a/stream/202961-General/topic/.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html b/stream/202961-General/topic/.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html
@@ -0,0 +1,32 @@
+<html>
+<head><meta charset="utf-8"><title>`quick_and_dirty` mode skips regular proofs · General · Zulip Chat Archive</title></head>
+<h2>Stream: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/index.html">General</a></h2>
+<h3>Topic: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html">`quick_and_dirty` mode skips regular proofs</a></h3>
+
+<hr>
+
+<base href="https://isabelle.zulipchat.com/">
+
+<head><link href="http://isabelle.systems/zulip-archive/style.css" rel="stylesheet"></head>
+
+<a name="272252199"></a>
+<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%60quick_and_dirty%60%20mode%20skips%20regular%20proofs/near/272252199" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Fabian Huch <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html#272252199">(Feb 17 2022 at 12:33)</a>:</h4>
+<p>When <code>quick_and_dirty</code> mode is enabled, some regular proofs get replaced with skip proofs (i.e. <code>sorry</code> oracles). For example, the following will throw an Exception when you <code>build</code> it (curiously, the interactive session works just fine):</p>
+<div class="codehilite" data-code-language="Isabelle"><pre><span></span><code><span class="k">fun</span> <span class="n">ex</span> <span class="o">::</span> <span class="s">"'a ⇒ nat"</span> <span class="kp">where</span>
+  <span class="s">"ex _ = 0"</span>
+
+<span class="kn">theorem</span> <span class="n">ex_const</span><span class="o">:</span> <span class="s">"ex 5 = ex 7"</span>
+  <span class="k">by</span> <span class="n">auto</span>
+
+<span class="k">ML</span> <span class="err">‹</span>
+<span class="n">exception</span> <span class="n">E</span><span class="err">;</span>
+<span class="kp">if</span> <span class="o">(</span><span class="n">Thm_Deps.has_skip_proof</span> <span class="o">[</span><span class="err">@</span><span class="ow">{</span><span class="kt">thm</span> <span class="n">ex_const</span><span class="ow">}</span><span class="o">])</span> <span class="k">then</span> <span class="n">raise</span> <span class="n">E</span>
+<span class="n">else</span> <span class="o">()</span>
+<span class="err">›</span>
+</code></pre></div>
+<p>Is there a reason for that? Or an option to disable this behavior?</p>
+
+
+
+<hr><p>Last updated: Jul 15 2022 at 23:21 UTC</p>
+</html>
diff --git a/stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html b/stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html
@@ -0,0 +1,41 @@
+<html>
+<head><meta charset="utf-8"><title>`rewrite` method tutorial · General · Zulip Chat Archive</title></head>
+<h2>Stream: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/index.html">General</a></h2>
+<h3>Topic: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html">`rewrite` method tutorial</a></h3>
+
+<hr>
+
+<base href="https://isabelle.zulipchat.com/">
+
+<head><link href="http://isabelle.systems/zulip-archive/style.css" rel="stylesheet"></head>
+
+<a name="191468106"></a>
+<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%60rewrite%60%20method%20tutorial/near/191468106" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Chen <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html#191468106">(Mar 23 2020 at 12:54)</a>:</h4>
+<p>I seem to recall that there was a PDF tutorial describing the <code>rewrite</code> method, does anyone know where it lives?</p>
+
+
+
+<a name="191475114"></a>
+<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%60rewrite%60%20method%20tutorial/near/191475114" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Kevin Kappelmann <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html#191475114">(Mar 23 2020 at 13:51)</a>:</h4>
+<p>Only thing I found is <a href="https://pdfs.semanticscholar.org/717e/4d3dbf9fe5fdef35df1c91152f1bd04d9b63.pdf" target="_blank" title="https://pdfs.semanticscholar.org/717e/4d3dbf9fe5fdef35df1c91152f1bd04d9b63.pdf">the paper</a> describing the subterm selection part of the tactic, but I guess that's not what you were looking for</p>
+
+
+
+<a name="191475265"></a>
+<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%60rewrite%60%20method%20tutorial/near/191475265" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Chen <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html#191475265">(Mar 23 2020 at 13:52)</a>:</h4>
+<p>Mm yeah I found that too, but somehow I have this memory of reading an actual tutorial for <code>rewrite</code>. Thanks though! :)</p>
+
+
+
+<a name="191655242"></a>
+<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%60rewrite%60%20method%20tutorial/near/191655242" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Simon Wimmer <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html#191655242">(Mar 24 2020 at 18:42)</a>:</h4>
+<p><span class="user-mention silent" data-user-id="233154">Kevin Kappelmann</span> <a href="#narrow/stream/202961-general/topic/.60rewrite.60.20method.20tutorial/near/191475114" title="#narrow/stream/202961-general/topic/.60rewrite.60.20method.20tutorial/near/191475114">said</a>:</p>
+<blockquote>
+<p>Only thing I found is <a href="https://pdfs.semanticscholar.org/717e/4d3dbf9fe5fdef35df1c91152f1bd04d9b63.pdf" target="_blank" title="https://pdfs.semanticscholar.org/717e/4d3dbf9fe5fdef35df1c91152f1bd04d9b63.pdf">the paper</a> describing the subterm selection part of the tactic, but I guess that's not what you were looking for</p>
+</blockquote>
+<p>Yes, I think this is the only source.</p>
+
+
+
+<hr><p>Last updated: Feb 10 2024 at 01:01 UTC</p>
+</html>
diff --git a/....9C.94.20.60.5C.3Ccomment.3E.60.20after.20.60text.60.20omitted.20in.20LaTeX.20output.html b/....9C.94.20.60.5C.3Ccomment.3E.60.20after.20.60text.60.20omitted.20in.20LaTeX.20output.html
@@ -0,0 +1,40 @@
+<html>
+<head><meta charset="utf-8"><title>✔ `\&lt;comment&gt;` after `text` omitted in LaTeX output · General · Zulip Chat Archive</title></head>
+<h2>Stream: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/index.html">General</a></h2>
+<h3>Topic: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.E2.9C.94.20.60.5C.3Ccomment.3E.60.20after.20.60text.60.20omitted.20in.20LaTeX.20output.html">✔ `\&lt;comment&gt;` after `text` omitted in LaTeX output</a></h3>
+
+<hr>
+
+<base href="https://isabelle.zulipchat.com/">
+
+<head><link href="http://isabelle.systems/zulip-archive/style.css" rel="stylesheet"></head>
+
+<a name="270589789"></a>
+<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%E2%9C%94%20%60%5C%3Ccomment%3E%60%20after%20%60text%60%20omitted%20in%20LaTeX%20output/near/270589789" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Max Jakobitsch <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.E2.9C.94.20.60.5C.3Ccomment.3E.60.20after.20.60text.60.20omitted.20in.20LaTeX.20output.html#270589789">(Feb 03 2022 at 17:48)</a>:</h4>
+<p>Marginal comments (<code>\&lt;comment&gt;</code>) normally are part of the LaTeX/PDF output, but are left out when they appear after <code>text</code> (and some other markup commands I have tried).</p>
+<div class="codehilite" data-code-language="Isabelle"><pre><span></span><code><span class="kt">term</span> <span class="n">A</span>
+
+<span class=" -Symbol">\&lt;comment&gt;</span> <span class=" -Symbol">\&lt;open&gt;</span><span class="n">Marginal</span> <span class="n">comments</span> <span class="n">should</span> <span class="n">appear</span> <span class="kp">in</span> <span class="n">LaTeX</span><span class="o">,</span> <span class="n">right</span><span class="o">?</span><span class=" -Symbol">\&lt;close&gt;</span>
+
+<span class="k">text</span><span class=" -Symbol">\&lt;open&gt;</span><span class="n">But</span> <span class="n">apparently</span> <span class="n">not</span> <span class="n">after</span> <span class="n">markup</span> <span class="n">commands.</span><span class=" -Symbol">\&lt;close&gt;</span>
+
+<span class=" -Symbol">\&lt;comment&gt;</span> <span class=" -Symbol">\&lt;open&gt;</span><span class="n">I'm</span> <span class="n">invisible</span><span class="o">!</span><span class=" -Symbol">\&lt;close&gt;</span>
+</code></pre></div>
+<p>Is this intended behavior?</p>
+
+
+
+<a name="270592317"></a>
+<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%E2%9C%94%20%60%5C%3Ccomment%3E%60%20after%20%60text%60%20omitted%20in%20LaTeX%20output/near/270592317" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Manuel Eberl <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.E2.9C.94.20.60.5C.3Ccomment.3E.60.20after.20.60text.60.20omitted.20in.20LaTeX.20output.html#270592317">(Feb 03 2022 at 18:05)</a>:</h4>
+<p>Sounds like it's not intended. It's best to report such things directly to the isabelle-users mailing list. This is something Makarius should know about, and he doesn't read Zulip.</p>
+
+
+
+<a name="270593521"></a>
+<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%E2%9C%94%20%60%5C%3Ccomment%3E%60%20after%20%60text%60%20omitted%20in%20LaTeX%20output/near/270593521" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Notification Bot <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.E2.9C.94.20.60.5C.3Ccomment.3E.60.20after.20.60text.60.20omitted.20in.20LaTeX.20output.html#270593521">(Feb 03 2022 at 18:14)</a>:</h4>
+<p><span class="user-mention silent" data-user-id="407560">Max Jakobitsch</span> has marked this topic as resolved.</p>
+
+
+
+<hr><p>Last updated: Feb 10 2024 at 01:01 UTC</p>
+</html>
diff --git a/...61-General/topic/.E2.9C.94.20.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html b/...61-General/topic/.E2.9C.94.20.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html
@@ -0,0 +1,44 @@
+<html>
+<head><meta charset="utf-8"><title>✔ `quick_and_dirty` mode skips regular proofs · General · Zulip Chat Archive</title></head>
+<h2>Stream: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/index.html">General</a></h2>
+<h3>Topic: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.E2.9C.94.20.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html">✔ `quick_and_dirty` mode skips regular proofs</a></h3>
+
+<hr>
+
+<base href="https://isabelle.zulipchat.com/">
+
+<head><link href="http://isabelle.systems/zulip-archive/style.css" rel="stylesheet"></head>
+
+<a name="272252199"></a>
+<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%E2%9C%94%20%60quick_and_dirty%60%20mode%20skips%20regular%20proofs/near/272252199" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Fabian Huch <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.E2.9C.94.20.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html#272252199">(Feb 17 2022 at 12:33)</a>:</h4>
+<p>When <code>quick_and_dirty</code> mode is enabled, some regular proofs get replaced with skip proofs (i.e. <code>sorry</code> oracles). For example, the following will throw an Exception when you <code>build</code> it (curiously, the interactive session works just fine):</p>
+<div class="codehilite" data-code-language="Isabelle"><pre><span></span><code><span class="k">fun</span> <span class="n">ex</span> <span class="o">::</span> <span class="s">"'a ⇒ nat"</span> <span class="kp">where</span>
+  <span class="s">"ex _ = 0"</span>
+
+<span class="kn">theorem</span> <span class="n">ex_const</span><span class="o">:</span> <span class="s">"ex 5 = ex 7"</span>
+  <span class="k">by</span> <span class="n">auto</span>
+
+<span class="k">ML</span> <span class="err">‹</span>
+<span class="n">exception</span> <span class="n">E</span><span class="err">;</span>
+<span class="kp">if</span> <span class="o">(</span><span class="n">Thm_Deps.has_skip_proof</span> <span class="o">[</span><span class="err">@</span><span class="ow">{</span><span class="kt">thm</span> <span class="n">ex_const</span><span class="ow">}</span><span class="o">])</span> <span class="k">then</span> <span class="n">raise</span> <span class="n">E</span>
+<span class="n">else</span> <span class="o">()</span>
+<span class="err">›</span>
+</code></pre></div>
+<p>Is there a reason for that? Or an option to disable this behavior?</p>
+
+
+
+<a name="272692571"></a>
+<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%E2%9C%94%20%60quick_and_dirty%60%20mode%20skips%20regular%20proofs/near/272692571" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Fabian Huch <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.E2.9C.94.20.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html#272692571">(Feb 21 2022 at 14:07)</a>:</h4>
+<p>Apparently <code>quick_and_dirty</code> also axiomatizes some datatype/function constructions (so that they are faster), which is the reason the above fails. Except for locally disabling <code>quick_and_dirty</code>, there does not seem to be an option to turn that off.</p>
+
+
+
+<a name="272692596"></a>
+<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%E2%9C%94%20%60quick_and_dirty%60%20mode%20skips%20regular%20proofs/near/272692596" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Notification Bot <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.E2.9C.94.20.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html#272692596">(Feb 21 2022 at 14:07)</a>:</h4>
+<p><span class="user-mention silent" data-user-id="348400">Fabian Huch</span> has marked this topic as resolved.</p>
+
+
+
+<hr><p>Last updated: Feb 10 2024 at 01:01 UTC</p>
+</html>