Skip to content

Commit

Permalink
Update archive.
Browse files Browse the repository at this point in the history
  • Loading branch information
Archive Bot committed Feb 10, 2024
0 parents commit f0d509f
Show file tree
Hide file tree
Showing 20,183 changed files with 1,283,640 additions and 0 deletions.
The diff you're trying to view is too large. We only load the first 3000 changed files.
20 changes: 20 additions & 0 deletions .github/workflows/main.yaml
Original file line number Diff line number Diff line change
@@ -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
Empty file added .nojekyll
Empty file.
10 changes: 10 additions & 0 deletions assets/img/zulip.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
42 changes: 42 additions & 0 deletions index.html
Original file line number Diff line number Diff line change
@@ -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 08:16 UTC</p>
</html>
Binary file added sitemap-001-pages.xml.gz
Binary file not shown.
6 changes: 6 additions & 0 deletions sitemap.xml
Original file line number Diff line number Diff line change
@@ -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>
279 changes: 279 additions & 0 deletions stream/202961-General/index.html

Large diffs are not rendered by default.

19 changes: 19 additions & 0 deletions stream/202961-General/topic/(no.20topic).html
Original file line number Diff line number Diff line change
@@ -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>

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
@@ -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>
41 changes: 41 additions & 0 deletions stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html
Original file line number Diff line number Diff line change
@@ -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 08:16 UTC</p>
</html>
Original file line number Diff line number Diff line change
@@ -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 08:16 UTC</p>
</html>
Original file line number Diff line number Diff line change
@@ -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 08:16 UTC</p>
</html>
Loading

0 comments on commit f0d509f

Please sign in to comment.