commit 6a41828133f4864feabbdcf6e4a3dc6457a07ea5 · anil.recoil.org/atomic-eeg

+48 -1

aggregate_feeds.py

···

       4
       4
        
       #   "feedparser",

     

       5
       5
        
       #   "feedgenerator",

     

       6
       6
        
       #   "requests",

     

       7
       7
       +
       #   "beautifulsoup4",

     

       7
       8
        
       # ]

     

       8
       9
        
       # ///

     

       9
       10
        
       # Do not delete the above as its needed for `uv run`

     
···

       17
       18
        
       import requests

     

       18
       19
        
       import sys

     

       19
       20
        
       import os

     

       21
       21
       +
       import re

     

       22
       22
       +
       from html import unescape

     

       23
       23
       +
       from bs4 import BeautifulSoup

     

       20
       24
        
       

     

       21
       25
        
       def load_feed_urls(file_path):

     

       22
       26
        
           with open(file_path, 'r') as f:

     
···

       48
       52
        
               print(f"Error fetching {url}: {e}", file=sys.stderr)

     

       49
       53
        
               return None

     

       50
       54
        
       

     

       55
       55
       +
       def create_plain_text_preview(html_content, max_length=500):

     

       56
       56
       +
           """

     

       57
       57
       +
           Create a plain text preview from HTML content, preserving hyperlinks

     

       58
       58
       +
           in the format: text [link_url]

     

       59
       59
       +
           """

     

       60
       60
       +
           if not html_content:

     

       61
       61
       +
               return ""

     

       62
       62
       +
           

     

       63
       63
       +
           # Parse HTML

     

       64
       64
       +
           soup = BeautifulSoup(html_content, 'html.parser')

     

       65
       65
       +
           

     

       66
       66
       +
           # Extract text and hyperlinks

     

       67
       67
       +
           text_parts = []

     

       68
       68
       +
           

     

       69
       69
       +
           # Process all elements

     

       70
       70
       +
           for element in soup.descendants:

     

       71
       71
       +
               if element.name == 'a' and element.get('href'):

     

       72
       72
       +
                   # For hyperlinks, preserve the URL

     

       73
       73
       +
                   text = element.get_text(strip=True)

     

       74
       74
       +
                   if text:

     

       75
       75
       +
                       url = element['href']

     

       76
       76
       +
                       text_parts.append(f"{text} [{url}]")

     

       77
       77
       +
               elif element.string and element.string.strip():

     

       78
       78
       +
                   # For regular text nodes

     

       79
       79
       +
                   text_parts.append(element.string.strip())

     

       80
       80
       +
           

     

       81
       81
       +
           # Join all text parts with spaces

     

       82
       82
       +
           preview = ' '.join(text_parts)

     

       83
       83
       +
           

     

       84
       84
       +
           # Clean up extra whitespace

     

       85
       85
       +
           preview = re.sub(r'\s+', ' ', preview).strip()

     

       86
       86
       +
           

     

       87
       87
       +
           # Truncate if needed

     

       88
       88
       +
           if len(preview) > max_length:

     

       89
       89
       +
               preview = preview[:max_length] + "..."

     

       90
       90
       +
           

     

       91
       91
       +
           return preview

     

       92
       92
       +
       

     

       51
       93
        
       def extract_entries(feeds):

     

       52
       94
        
           all_entries = []

     

       53
       95
        
           for feed_data in feeds:

     
···

       87
       129
        
                   else:

     

       88
       130
        
                       content = entry.get('summary', '')

     

       89
       131
        
                   

     

       132
       132
       +
                   # Create plain text preview

     

       133
       133
       +
                   preview = create_plain_text_preview(content)

     

       134
       134
       +
                   

     

       90
       135
        
                   # Get unique ID

     

       91
       136
        
                   entry_id = entry.get('id', link)

     

       92
       137
        
                   

     
···

       94
       139
        
                       'title': title,

     

       95
       140
        
                       'link': link,

     

       96
       141
        
                       'content': content,

     

       142
       142
       +
                       'preview': preview,

     

       97
       143
        
                       'author': author_name,

     

       98
       144
        
                       'pub_date': pub_date,

     

       99
       145
        
                       'feed_title': feed_title,

     
···

       132
       178
        
                   categories=[entry['feed_title']],  # Use feed title as category for attribution

     

       133
       179
        
                   # Add formatted date as extra field

     

       134
       180
        
                   updateddate=entry['pub_date'],

     

       135
       135
       -
                   formatted_date=formatted_date

     

       181
       181
       +
                   formatted_date=formatted_date,

     

       182
       182
       +
                   preview=entry['preview']  # Add the plain text preview

     

       136
       183
        
               )

     

       137
       184
        
           

     

       138
       185
        
           return feed

+1 -159

eeg.xml

···

       71
       71
        
         &lt;li&gt;10 x Kingston 7.68TB SSD&lt;/li&gt;

     

       72
       72
        
       &lt;/ul&gt;

     

       73
       73
        
       

     

       74
       74
       -
       &lt;p&gt;&lt;a href="https://www.dell.com/support/manuals/en-uk/poweredge-r640/per640_ism_pub/general-memory-module-installation-guidelines?guid=guid-acbc0f13-dedb-492b-a0b0-18303ded565a&amp;amp;lang=en-us"&gt;Dell R640 has 24 DIMM slots&lt;/a&gt;&lt;/p&gt;</summary><category term="Tunbury.ORG"></category></entry><entry><title>Weeknotes 2025-W15</title><link href="https://www.jonmsterling.com/2025-W15/" rel="alternate"></link><published>2025-04-09T13:53:56Z</published><updated>2025-04-09T13:53:56Z</updated><author><name>JonS</name></author><id>https://www.jonmsterling.com/2025-W15/</id><summary type="html">&lt;p&gt;I have a lot to say this week, so strap in.&lt;/p&gt;

     

       75
       75
       -
               &lt;section&gt;

     

       76
       76
       -
                 &lt;header&gt;

     

       77
       77
       -
                   &lt;h2&gt;&lt;a href="https://www.forester-notes.org/jms-011P/"&gt;Forester 5.0&lt;/a&gt; development: canonical URLs, atom feeds, and LSP&lt;/h2&gt;

     

       78
       78
       -
                 &lt;/header&gt;

     

       79
       79
       -
                 &lt;p&gt;Work on &lt;a href="https://www.forester-notes.org/jms-011P/"&gt;Forester 5.0&lt;/a&gt; proceeds apace, generously supported by &lt;a href="https://www.jonmsterling.com/jms-00XB/"&gt;ARIA&lt;/a&gt; who have engaged &lt;a href="https://www.jonmsterling.com/kentookura/"&gt;Kento Okura&lt;/a&gt; and myself on a consulting basis to support their internal use of Forester. My recent goals have been to bring Forester closer in line with the architecture of the World Wide Web; to that end, I have made two big improvements.&lt;/p&gt;

     

       80
       80
       -
                 &lt;section&gt;

     

       81
       81
       -
                   &lt;header&gt;

     

       82
       82
       -
                     &lt;h3&gt;First cut at canonical URLs&lt;/h3&gt;

     

       83
       83
       -
                   &lt;/header&gt;

     

       84
       84
       -
                   &lt;p&gt;Trees are addressed by “canonical URLs” that are meant to be the place where they will ultimately be published. See &lt;a href="https://www.forester-notes.org/JVIT/"&gt;my blog post&lt;/a&gt; on the design for more details. Canonical URLs are of the form &lt;code&gt;https://www.my-host.net/tree-name/&lt;/code&gt;; the handling is a little fragile right now and you can expect bugs (but please write to me about them).&lt;/p&gt;

     

       85
       85
       -
                 &lt;/section&gt;

     

       86
       86
       -
                 &lt;section&gt;

     

       87
       87
       -
                   &lt;header&gt;

     

       88
       88
       -
                     &lt;h3&gt;First cut at atom syndication&lt;/h3&gt;

     

       89
       89
       -
                   &lt;/header&gt;

     

       90
       90
       -
                   &lt;p&gt;It is now possible to syndicate the children of a tree as an Atom feed. This is done currently by including the following directive in the tree you wish to syndicate:&lt;/p&gt;

     

       91
       91
       -
                   &lt;pre&gt;\syndicate-current-tree-as-atom-feed&lt;/pre&gt;

     

       92
       92
       -
                   &lt;p&gt;Then, if your tree is located at &lt;code&gt;https://www.my-host.net/tree-name/&lt;/code&gt;, you will find that there is an atom feed at &lt;code&gt;https://www.my-host.net/tree-name/atom.xml&lt;/code&gt;. There are many subtleties to this, and the atom support will continue to evolve and improve. One thing I need to deal with is the fact that Forester produces nested hyperlinks—which are not valid in HTML! I came up with a pretty slick way to &lt;a href="https://git.sr.ht/~jonsterling/forester-base-theme/commit/a251f9cf19b0ff42f4553d315df5181b985c79cb"&gt;handle this in XSLT&lt;/a&gt;, but that Atom renderer is intended to bypass that entirely.&lt;/p&gt;

     

       93
       93
       -
                   &lt;p&gt;As a side note, I am very happy to see that I am &lt;a href="https://patrick.sirref.org/weekly-2025-03-31/"&gt;not the only person&lt;/a&gt; using the new support for Atom feeds. Patrick’s fork of Forester is looking pretty cool, and I am excited to learn more from what he is doing. I’m also relieved that he was able to get rebased atop the ever-changing &lt;code&gt;forester-5.0-dev&lt;/code&gt; branch.&lt;/p&gt;

     

       94
       94
       -
                 &lt;/section&gt;

     

       95
       95
       -
                 &lt;section&gt;

     

       96
       96
       -
                   &lt;header&gt;

     

       97
       97
       -
                     &lt;h3&gt;Federation is still janky&lt;/h3&gt;

     

       98
       98
       -
                   &lt;/header&gt;

     

       99
       99
       -
                   &lt;p&gt;One thing I want to start designing soon is how best to handle federated forests. Right now, Forester bundles all the imported material under a &lt;code&gt;foreign/my-friends-host/&lt;/code&gt; directory and routes all links accordingly, but in many (but not all!) cases one would want to not bundle things at all and instead have links routed directly to the canonical URLs as published on the World Wide Web. I am not sure of the best design for this, so I welcome feedback. In the meanwhile, enjoy the janky prototype feel.&lt;/p&gt;

     

       100
       100
       -
                 &lt;/section&gt;

     

       101
       101
       -
                 &lt;section&gt;

     

       102
       102
       -
                   &lt;header&gt;

     

       103
       103
       -
                     &lt;h3&gt;Language server; code completion via effects and handlers&lt;/h3&gt;

     

       104
       104
       -
                   &lt;/header&gt;

     

       105
       105
       -
                   &lt;p&gt;&lt;a href="https://www.jonmsterling.com/kentookura/"&gt;Kento&lt;/a&gt; is hard at work hardening Forester’s language server. I am hoping that we will have something to show on the scale of a week.&lt;/p&gt;

     

       106
       106
       -
                   &lt;p&gt;There were some subtleties about how to provide completion information at a source location—which is at least as complex as the expander itself, since scope emerges from the expansion process. We had something fairly broken in place, which I have spent Thursday and Friday morning replacing with something cool using OCaml 5’s effects and handlers. The idea is to instrument the expander with an effect that notifies observes that it has entered a source range; this can be handled as a no-op, &lt;em&gt;or&lt;/em&gt; by querying the scope’s available symbols when it enters the desired range and throwing away the continuation, and resuming the continuation otherwise to keep searching. This approach allows all the scope-handling code to be unified into a single routine, whose behaviour is controlled by effect handlers on the outside.&lt;/p&gt;

     

       107
       107
       -
                   &lt;p&gt;As a side note, I am looking forward to when the next version of &lt;a href="https://topiary.tweag.io/"&gt;Topiary&lt;/a&gt; is released, which should contain support for formatting OCaml’s effect handlers. Right now we don’t use the nice notation because we are stuck on Topiary 0.6.0.&lt;/p&gt;

     

       108
       108
       -
                 &lt;/section&gt;

     

       109
       109
       -
               &lt;/section&gt;

     

       110
       110
       -
               &lt;section&gt;

     

       111
       111
       -
                 &lt;header&gt;

     

       112
       112
       -
                   &lt;h2&gt;&lt;a href="https://www.jonmsterling.com/jms-019E/"&gt;Project Pterosaur&lt;/a&gt;: yes, I’m building a new proof assistant&lt;/h2&gt;

     

       113
       113
       -
                 &lt;/header&gt;

     

       114
       114
       -
                 &lt;p&gt;I swore after building &lt;a href="https://github.com/RedPRL/cooltt"&gt;cooltt&lt;/a&gt;, &lt;a href="https://github.com/RedPRL/redtt"&gt;redtt&lt;/a&gt;, and &lt;a href="https://github.com/RedPRL/sml-redprl"&gt;RedPRL&lt;/a&gt; that I would never build another proof assistant, as the experience burned around four years of my PhD and resulted (at least directly) in very little publishable work—but, to be fair, I probably would not have made the &lt;a href="https://www.jonmsterling.com/jms-0014/"&gt;key mathematical discovery&lt;/a&gt; of my &lt;a href="https://www.jonmsterling.com/sterling-2021-thesis/"&gt;PhD thesis&lt;/a&gt; if it were not for these engineering experiments. But I’m back on my bullshit, as the young people say, and hard at work building a new interactive proof assistant that I have code-named &lt;a href="https://www.jonmsterling.com/jms-019E/"&gt;Project Pterosaur&lt;/a&gt;.&lt;/p&gt;

     

       115
       115
       -
                 &lt;section&gt;

     

       116
       116
       -
                   &lt;header&gt;

     

       117
       117
       -
                     &lt;h3&gt;Locales in dependent type theory?&lt;/h3&gt;

     

       118
       118
       -
                   &lt;/header&gt;

     

       119
       119
       -
                   &lt;p&gt;The goal of Pterosaur is to explore the adaptation of &lt;em&gt;locales&lt;/em&gt; from Isabelle to dependent type theory, as a lightweight but extremely expressive alternative to type classes. My colleague &lt;a href="https://www.jonmsterling.com/lawrencepaulson/"&gt;Larry Paulson&lt;/a&gt; has written &lt;a href="https://lawrencecpaulson.github.io/tag/locales"&gt;some great blog posts about locales in Isabelle&lt;/a&gt;, and I strongly recommend reading Ballarin’s &lt;a href="https://www21.in.tum.de/~ballarin/publications/jar2019.pdf"&gt;Exploring the Structure of an Algebra Text with Locales&lt;/a&gt; to get a feel for what is possible. Here is what locales do:&lt;/p&gt;

     

       120
       120
       -
                   &lt;ol&gt;&lt;li&gt;Locales appear to completely solve the pain involved when building up hierarchies of mathematical structures and notations, allowing you to effortlessly combine theories along a common core (e.g. defining rings in terms of a multiplicative monoid and an Abelian group sharing the same carrier).&lt;/li&gt;

     

       121
       121
       -
             &lt;li&gt;Locales allow you to &lt;em&gt;add new methods&lt;/em&gt; to a theory after the fact, and they will magically be available on anything that extended that theory. You can also add new links in the theory graph, and both cycles and diamonds are allowed so long as they are coherent; this is useful if you want to silently regard (e.g.) the space of endomaps on a set as a monoid, etc.&lt;/li&gt;&lt;/ol&gt;

     

       122
       122
       -
                   &lt;p&gt;In comparison to modules and type classes, the strength of locales is that you don’t have to decide ahead of time whether you want to “bundle” fields with their carriers, etc. In contrast, a great deal of the difficult work of mathematical library design and maintainance in tools like Rocq, Agda, and &lt;a href="https://www.jonmsterling.com/jms-019G/"&gt;Lean&lt;/a&gt; is figuring out just what things to bundle, and fixing things when your choices inevitably lead to breakage, etc. Locales avoid these problems entirely.&lt;/p&gt;

     

       123
       123
       -
                   &lt;p&gt;Finally, a reasonably usable locale implementation can be obtained &lt;em&gt;without any higher-order unification whatsoever&lt;/em&gt;. I have a feeling that will be extremely important, given how unreliable (and &lt;a href="https://github.com/agda/agda/issues/5837"&gt;incorrect&lt;/a&gt;!) most implementations of higher-order unification are; the situation is so bad that it is actually an open problem to define a correct higher-order unification algorithm in the presence of singleton types (such as the unit type). I do think that this can be solved (and may have already been solved by Andras Kovacs), but my point is that the prognosis for unification in dependent type theory is bad.&lt;/p&gt;

     

       124
       124
       -
                 &lt;/section&gt;

     

       125
       125
       -
                 &lt;section&gt;

     

       126
       126
       -
                   &lt;header&gt;

     

       127
       127
       -
                     &lt;h3&gt;Experimental implementation in &lt;a href="https://www.jonmsterling.com/jms-019G/"&gt;Lean&lt;/a&gt;&lt;/h3&gt;

     

       128
       128
       -
                   &lt;/header&gt;

     

       129
       129
       -
                   &lt;p&gt;The other interesting thing about Pterosaur is that I am implementing it in &lt;a href="https://www.jonmsterling.com/jms-019G/"&gt;Lean&lt;/a&gt;; I am not verifying anything, and am making free use of Lean’s &lt;code&gt;partial&lt;/code&gt; keyword (which hides potentially divergent code from definitional equality). Instead, I am thinking of Lean as a “better OCaml”: I can’t speak to the quality of the compiler and code generator, but I can absolutely say that from the perspective of day-to-day programming, Lean has a lot of affordances that make it extremely nice to use. On the other hand, Lean’s story for modularity is not so good; but I hope they don’t “fix” it any time soon, because I think that something like locales could be a good option for Lean itself in the future if I am able to demonstrate their potential in the context of Pterosaur’s clean-room implementation.&lt;/p&gt;

     

       130
       130
       -
                 &lt;/section&gt;

     

       131
       131
       -
                 &lt;section&gt;

     

       132
       132
       -
                   &lt;header&gt;

     

       133
       133
       -
                     &lt;h3&gt;A taste of code&lt;/h3&gt;

     

       134
       134
       -
                   &lt;/header&gt;

     

       135
       135
       -
                   &lt;p&gt;I will have more to say about Pterosaur in the future, but let me leave you with a bit of demo code.&lt;/p&gt;

     

       136
       136
       -
                   &lt;pre&gt;locale Magma { A =&amp;gt;

     

       137
       137
       -
         car : Type,

     

       138
       138
       -
         car.isSet : isSet A·car,

     

       139
       139
       -
         cmp : (x y : A·car) → A·car

     

       140
       140
       -
       }

     

       141
       141
       -
       

     

       142
       142
       -
       locale Magma.Hom { f =&amp;gt;

     

       143
       143
       -
         dom : Magma,

     

       144
       144
       -
         cod : Magma,

     

       145
       145
       -
         car : (x : f·dom·car) → f·cod·car,

     

       146
       146
       -
         cmp : (x y : f·dom·car) → Id f·cod·car (f·car (f·dom·cmp x y)) (f·cod·cmp (f·car x) (f·car y))

     

       147
       147
       -
       }

     

       148
       148
       -
       

     

       149
       149
       -
       locale Semigroup { A =&amp;gt;

     

       150
       150
       -
         splice magma : Magma,

     

       151
       151
       -
         cmp.assoc : (x y z : A·car) → Id A·car (A·cmp (A·cmp x y) z) (A·cmp x (A·cmp y z))

     

       152
       152
       -
       }

     

       153
       153
       -
       

     

       154
       154
       -
       locale Semigroup.Hom {f =&amp;gt;

     

       155
       155
       -
         dom : Semigroup,

     

       156
       156
       -
         cod : Semigroup,

     

       157
       157
       -
         splice magma.hom : Magma.Hom / {dom := f·dom·magma, cod := f·cod·magma}

     

       158
       158
       -
       }

     

       159
       159
       -
       

     

       160
       160
       -
       locale Monoid { A =&amp;gt;

     

       161
       161
       -
         splice semigroup : Semigroup,

     

       162
       162
       -
         unit : A·car,

     

       163
       163
       -
         cmp.leftUnit : (x : A·car) → Id A·car (A·cmp A·unit x) x,

     

       164
       164
       -
         cmp.rightUnit : (x : A·car) → Id A·car (A·cmp x A·unit) x

     

       165
       165
       -
       }

     

       166
       166
       -
       

     

       167
       167
       -
       locale Monoid.Hom {f =&amp;gt;

     

       168
       168
       -
         dom : Monoid,

     

       169
       169
       -
         cod : Monoid,

     

       170
       170
       -
         splice semigroup.hom : Semigroup.Hom / {dom := f·dom·semigroup, cod := f·cod·semigroup},

     

       171
       171
       -
         unit : Id f·cod·car (f·car f·dom·unit) f·cod·unit

     

       172
       172
       -
       }

     

       173
       173
       -
       

     

       174
       174
       -
       locale Group { G =&amp;gt;

     

       175
       175
       -
         splice monoid : Monoid,

     

       176
       176
       -
         inv : (x : G·car) → G·car,

     

       177
       177
       -
         inv.inv : (x : G·car) → Id G·car (G·inv (G·inv x)) x

     

       178
       178
       -
       }

     

       179
       179
       -
       

     

       180
       180
       -
       locale AbelianGroup { A =&amp;gt;

     

       181
       181
       -
         splice group : Group,

     

       182
       182
       -
         splice commutativeOperation : CommutativeOperation / {car := A·car, cmp := A·cmp}

     

       183
       183
       -
       }&lt;/pre&gt;

     

       184
       184
       -
                 &lt;/section&gt;

     

       185
       185
       -
               &lt;/section&gt;

     

       186
       186
       -
               &lt;section&gt;

     

       187
       187
       -
                 &lt;header&gt;

     

       188
       188
       -
                   &lt;h2&gt;Two papers to appear in &lt;a href="https://www.jonmsterling.com/lics-2025/"&gt;LICS ’25&lt;/a&gt;&lt;/h2&gt;

     

       189
       189
       -
                 &lt;/header&gt;

     

       190
       190
       -
                 &lt;p&gt;This week I have had two papers accepted at &lt;a href="https://www.jonmsterling.com/lics-2025/"&gt;LICS ’25&lt;/a&gt;; I’m excited about both of them.&lt;/p&gt;

     

       191
       191
       -
                 &lt;section&gt;

     

       192
       192
       -
                   &lt;header&gt;

     

       193
       193
       -
                     &lt;h3&gt;With &lt;a href="https://www.jonmsterling.com/leonipugh/"&gt;Leoni Pugh&lt;/a&gt;: &lt;a href="https://www.jonmsterling.com/pugh-sterling-2025/"&gt;When is the partial map classifier a Sierpiński cone?&lt;/a&gt;&lt;/h3&gt;

     

       194
       194
       -
                   &lt;/header&gt;

     

       195
       195
       -
                   &lt;p&gt;&lt;a href="https://www.jonmsterling.com/leonipugh/"&gt;Leoni Pugh&lt;/a&gt; is my old Part III student from 2023–2024, and this work builds on her Part III dissertation. The goal of our paper was to better understand the relationship between two approaches to partial functions in denotational semantics:&lt;/p&gt;

     

       196
       196
       -
                   &lt;ol&gt;&lt;li&gt;&lt;strong&gt;“Geometrical” partiality / “the Sierpiński cone”&lt;/strong&gt;: freely add a lowest element to the space representing a given data type. This is useful for defining functions whose &lt;em&gt;inputs&lt;/em&gt; are partially defined, because you can do a case-analysis on the definedness of the input.&lt;/li&gt;

     

       197
       197
       -
             &lt;li&gt;&lt;strong&gt;“Logical” partiality / “the partial map classifier”&lt;/strong&gt;: representing partially defined elements of a space &lt;math xmlns="http://www.w3.org/1998/Math/MathML"&gt;&lt;mi&gt;X&lt;/mi&gt;&lt;/math&gt; by pairs 

     

       198
       198
       -
         &lt;math xmlns="http://www.w3.org/1998/Math/MathML"&gt;&lt;mrow&gt;

     

       199
       199
       -
          &lt;mo fence="true"&gt;(&lt;/mo&gt;

     

       200
       200
       -
          &lt;mi&gt;p&lt;/mi&gt;&lt;mo&gt;,&lt;/mo&gt;&lt;mi&gt;x&lt;/mi&gt;

     

       201
       201
       -
          &lt;mo fence="true"&gt;)&lt;/mo&gt;

     

       202
       202
       -
         &lt;/mrow&gt;&lt;/math&gt;

     

       203
       203
       -
         where &lt;math xmlns="http://www.w3.org/1998/Math/MathML"&gt;&lt;mi&gt;p&lt;/mi&gt;&lt;/math&gt; is a proposition and &lt;math xmlns="http://www.w3.org/1998/Math/MathML"&gt;&lt;mi&gt;x&lt;/mi&gt;&lt;/math&gt; is a function from &lt;math xmlns="http://www.w3.org/1998/Math/MathML"&gt;&lt;mrow&gt;&lt;mi&gt;isTrue&lt;/mi&gt;

     

       204
       204
       -
         &lt;mrow&gt;

     

       205
       205
       -
          &lt;mo fence="true"&gt;(&lt;/mo&gt;

     

       206
       206
       -
          &lt;mi&gt;p&lt;/mi&gt;

     

       207
       207
       -
          &lt;mo fence="true"&gt;)&lt;/mo&gt;

     

       208
       208
       -
         &lt;/mrow&gt;

     

       209
       209
       -
        &lt;/mrow&gt;&lt;/math&gt; to &lt;math xmlns="http://www.w3.org/1998/Math/MathML"&gt;&lt;mi&gt;X&lt;/mi&gt;&lt;/math&gt;. This is useful for defining functions whose &lt;em&gt;outputs&lt;/em&gt; are partially defined.&lt;/li&gt;&lt;/ol&gt;

     

       210
       210
       -
                   &lt;p&gt;In traditional domain theory as developed by &lt;a href="https://www.jonmsterling.com/danascott/"&gt;Scott&lt;/a&gt;, the two kinds of partiality coincide—&lt;a href="https://www.jonmsterling.com/sterling-2024-lifting/"&gt;even constructively&lt;/a&gt;. I am, however, interested in &lt;a href="https://www.jonmsterling.com/hyland-1991/"&gt;&lt;em&gt;synthetic domain theory&lt;/em&gt;&lt;/a&gt; which abstracts away from continuity and limits and lets you just use sets and functions rather than cpos and continuous functions—provided that you avoid non-constructive principles like the Axiom of Choice or the Law of Excluded Middle. The starting point of our work is my observation that the two notions cannot coincide &lt;em&gt;absolutely&lt;/em&gt; in synthetic domain theory, but that there may be restricted subuniverses in which they do coincide. The main result of our paper is to define such a subuniverse, made possible by my discovery of the &lt;em&gt;based Segal condition&lt;/em&gt;—a strengthening of the usual Segal condition for higher categories.&lt;/p&gt;

     

       211
       211
       -
                   &lt;p&gt;A broader motivation of this work is to develop synthetic domain theory and synthetic higher category theory within the same framework. Whereas synthetic domain theory traditionally concerned itself with spaces that behaved like ω-complete partial orders (but where all functions are automatically monotone and continuous), the same ideas (if applied within &lt;a href="https://www.jonmsterling.com/hottbook/"&gt;homotopy type theory&lt;/a&gt;) allow you to consider spaces that behave like &lt;em&gt;∞-categories&lt;/em&gt; with colimits of ω-chains (but where all functions are automatically ∞-functorial and ω-continuous). I believe that unifying domain theory and higher category theory will prove useful for studying things like the denotational semantics of concurrency, which is inherently higher-dimensional.&lt;/p&gt;

     

       212
       212
       -
                 &lt;/section&gt;

     

       213
       213
       -
                 &lt;section&gt;

     

       214
       214
       -
                   &lt;header&gt;

     

       215
       215
       -
                     &lt;h3&gt;With &lt;a href="https://www.jonmsterling.com/andrewslattery/"&gt;Andrew Slattery&lt;/a&gt;: &lt;a href="https://www.jonmsterling.com/slattery-sterling-2025/"&gt;Hofmann–Streicher lifting of fibred categories&lt;/a&gt;&lt;/h3&gt;

     

       216
       216
       -
                   &lt;/header&gt;

     

       217
       217
       -
                   &lt;p&gt;This year, &lt;a href="https://www.jonmsterling.com/thomasstreicher/"&gt;Thomas Streicher&lt;/a&gt; (born 1958) passed away from cancer. Thomas was one of the Greats of dependent type theory and he also wrote an &lt;a href="https://www.abebooks.co.uk/9789812701428/Domain-theoretic-Foundations-Functional-Programming-Streicher-9812701427/plp"&gt;excellent textbook on domain theory for denotational semantics&lt;/a&gt;, but much more importantly he was kind and curious and patient and always made time for young people. While I was still finding my place in the community, Thomas was very generous to me with his time and advice, and he sent me many papers to referee.&lt;/p&gt;

     

       218
       218
       -
                   &lt;p&gt;Although Thomas made many contributions to dependent type theory, domain theory, realisability theory, and category theory, he is most known to type theorists for two things—both in collaboration with the late &lt;a href="https://www.jonmsterling.com/martinhofmann/"&gt;Martin Hofmann&lt;/a&gt;: the &lt;a href="https://www.jonmsterling.com/hofmann-streicher-1998/"&gt;groupoid interpretation of type theory&lt;/a&gt; and the eponymous  &lt;a href="https://www.jonmsterling.com/hofmann-streicher-1997/"&gt;Hofmann–Streicher universe lifting construction&lt;/a&gt;. Andrew and my paper pertains to the latter.&lt;/p&gt;

     

       219
       219
       -
                   &lt;p&gt;The idea of Hofmann–Streicher lifting has to do with universes, which are “types of types” (typically defined in such a way as to avoid paradoxes). Martin-Löf type theory usually includes universes in order to be able to quantify over (small enough) types; in the simplest models of Martin-Löf type theory, types are interpreted as sets and so Martin-Löf’s universes are interpreted as certain sets of sets, such as &lt;a href="https://www.jonmsterling.com/sga-4/"&gt;Grothendieck universes&lt;/a&gt;. But it is important to be able to interpret the language of type theory in more sophisticated worlds than set theory: for example, in &lt;em&gt;presheaves&lt;/em&gt; (which are functors from a fixed category &lt;math xmlns="http://www.w3.org/1998/Math/MathML"&gt;&lt;mi&gt;C&lt;/mi&gt;&lt;/math&gt; into &lt;math xmlns="http://www.w3.org/1998/Math/MathML"&gt;&lt;mi&gt;Set&lt;/mi&gt;&lt;/math&gt;).  What &lt;a href="https://www.jonmsterling.com/hofmann-streicher-1997/"&gt;Hofmann and Streicher&lt;/a&gt; did is show how to transform any universe of sets into a universe of presheaves!&lt;/p&gt;

     

       220
       220
       -
                   &lt;p&gt;Although Hofmann and Streicher’s construction worked well and had good properties, they did not find a &lt;em&gt;universal property&lt;/em&gt; for it—which is an abstract description of the object that determines it uniquely up to isomorphism, usually in terms of how it relates to other objects. Recently &lt;a href="https://www.jonmsterling.com/awodey-2024-universes/"&gt;Awodey&lt;/a&gt; found a 1-dimensional universal property, which was the starting point of our work. What Andrew and I wanted to do is generalise Awodey’s analysis in two directions:&lt;/p&gt;

     

       221
       221
       -
                   &lt;ol&gt;&lt;li&gt;We wanted a &lt;em&gt;2-dimensional&lt;/em&gt; version, which is useful because it captures more about the universe than can be said in just one dimension: for example, with a 2-dimensional version, you can see immediately (by “abstract nonsense”) that Hofmann–Streicher lifting preserves structures like monads, adjunctions, etc. that might be used for modelling computational effects, etc.&lt;/li&gt;

     

       222
       222
       -
             &lt;li&gt;We wanted a &lt;em&gt;relative&lt;/em&gt; version, which would make it easier to iterate the Hofmann–Streicher lifting construction: the purpose of this is to be able to define presheaf models of type theory &lt;em&gt;internal&lt;/em&gt; to other presheaf models. These kind of situations actually happen in practice! For example, the model of &lt;a href="https://www.jonmsterling.com/bbcgsv-2019/"&gt;guarded cubical type theory&lt;/a&gt; that combines step-indexing with univalence ought to be an example of this.&lt;/li&gt;&lt;/ol&gt;

     

       223
       223
       -
                   &lt;p&gt;To develop this two-fold generalisation of Hofmann–Streicher lifting, we resituated the theory in terms of another of Thomas’s favourite topics: the theory of &lt;em&gt;fibrations&lt;/em&gt;, on which Thomas had written &lt;a href="https://www.jonmsterling.com/streicher-fcjb/"&gt;the most wonderful lecture notes&lt;/a&gt;.&lt;/p&gt;

     

       224
       224
       -
                   &lt;p&gt;We dedicated our paper to Thomas’s memory. May he rest in peace.&lt;/p&gt;

     

       225
       225
       -
                 &lt;/section&gt;

     

       226
       226
       -
               &lt;/section&gt;

     

       227
       227
       -
               &lt;section&gt;

     

       228
       228
       -
                 &lt;header&gt;

     

       229
       229
       -
                   &lt;h2&gt;Personal, reading&lt;/h2&gt;

     

       230
       230
       -
                 &lt;/header&gt;

     

       231
       231
       -
                 &lt;p&gt;I recently read Arthur C. Clarke’s &lt;a href="https://www.jonmsterling.com/clarke-1979/"&gt;The Fountains of Paradise&lt;/a&gt;; although it was a pretty good read, I found that like many science fiction books of that era, one has to look past a lot in order to enjoy it. I wrote some commentary in my post entitled &lt;a href="https://www.jonmsterling.com/jms-019W/"&gt;Ventriloquy of the Mid-Century Man&lt;/a&gt; on my culture blog &lt;a href="https://www.jonmsterling.com/jms-015X/"&gt;The Jon Sterling Review of Books&lt;/a&gt;.&lt;/p&gt;

     

       232
       232
       -
               &lt;/section&gt;</summary><category term="Jon Sterling › Weeknotes"></category></entry><entry><title>Coping and Capping</title><link href="https://mort.io/blog/coping-and-capping/" rel="alternate"></link><published>2025-04-08T01:00:00Z</published><updated>2025-04-08T01:00:00Z</updated><author><name>RichardM</name></author><id>https://mort.io/blog/coping-and-capping/</id><summary type="html">&lt;p&gt;Well that was fun! Quite high up there in the set of things that I never even

     

       74
       74
       +
       &lt;p&gt;&lt;a href="https://www.dell.com/support/manuals/en-uk/poweredge-r640/per640_ism_pub/general-memory-module-installation-guidelines?guid=guid-acbc0f13-dedb-492b-a0b0-18303ded565a&amp;amp;lang=en-us"&gt;Dell R640 has 24 DIMM slots&lt;/a&gt;&lt;/p&gt;</summary><category term="Tunbury.ORG"></category></entry><entry><title>Coping and Capping</title><link href="https://mort.io/blog/coping-and-capping/" rel="alternate"></link><published>2025-04-08T01:00:00Z</published><updated>2025-04-08T01:00:00Z</updated><author><name>RichardM</name></author><id>https://mort.io/blog/coping-and-capping/</id><summary type="html">&lt;p&gt;Well that was fun! Quite high up there in the set of things that I never even

     

       233
       75
        
       considered I might do would’ve been awarding degrees. But by dint of being

     

       234
       76
        
       President and thus standing in for

     

       235
       77
        
       &lt;a href="https://en.wikipedia.org/wiki/Simon_McDonald%2C_Baron_McDonald_of_Salford"&gt;Simon&lt;/a&gt;,

+56 -2

index.html

···

       414
       414
        
                   max-height: none;

     

       415
       415
        
                   display: inline;

     

       416
       416
        
                   margin-left: 8px;

     

       417
       417
       +
                   opacity: 1;

     

       417
       418
        
               }

     

       418
       419
        
               

     

       419
       420
        
               .preview-links,

     
···

       1273
       1274
        
                           const firstLine = getFirstLine(contentHtml);

     

       1274
       1275
        
                           const textPreview = getTextPreview(contentHtml);

     

       1275
       1276
        
                           

     

       1277
       1277
       +
                           // Get preview from the entry directly (if available)

     

       1278
       1278
       +
                           const preview = entry.getElementsByTagName('preview')[0]?.textContent || '';

     

       1279
       1279
       +
                           

     

       1276
       1280
        
                           // Store the entry data

     

       1277
       1281
        
                           entriesById[id] = {

     

       1278
       1282
        
                               id,

     
···

       1280
       1284
        
                               title,

     

       1281
       1285
        
                               link,

     

       1282
       1286
        
                               contentHtml,

     

       1283
       1283
       -
                               firstLine,

     

       1287
       1287
       +
                               firstLine: preview || firstLine, // Use preview field if available, otherwise fallback to firstLine

     

       1284
       1288
        
                               textPreview,

     

       1285
       1289
        
                               published,

     

       1286
       1290
        
                               author,

     
···

       1431
       1435
        
                                       <div class="feed-item-date">${getDayWithOrdinal(date)}</div>

     

       1432
       1436
        
                                       <div class="feed-item-author">${entry.author}</div>

     

       1433
       1437
        
                                       <div class="feed-item-content-wrapper">

     

       1434
       1434
       -
                                           <div class="feed-item-title"><a href="${entry.link}" target="_blank">${entry.title}</a></div><div class="feed-item-preview">${entry.textPreview}</div>

     

       1438
       1438
       +
                                           <div class="feed-item-title"><a href="${entry.link}" target="_blank">${entry.title}</a></div><div class="feed-item-preview">${entry.firstLine}</div>

     

       1435
       1439
        
                                           

     

       1436
       1440
        
                                           ${entry.externalLinks && entry.externalLinks.length > 0 ? `

     

       1437
       1441
        
                                           <div class="preview-links">

     
···

       1660
       1664
        
                           header.style.visibility = index === 0 ? 'visible' : 'hidden';

     

       1661
       1665
        
                       });

     

       1662
       1666
        
                       

     

       1667
       1667
       +
                       // If we have entries, set the most recent (first) entry's date as active in the timeline

     

       1668
       1668
       +
                       if (entriesArray.length > 0) {

     

       1669
       1669
       +
                           const mostRecentEntry = entriesArray[0];

     

       1670
       1670
       +
                           const date = new Date(mostRecentEntry.published);

     

       1671
       1671
       +
                           const year = date.getFullYear();

     

       1672
       1672
       +
                           const month = date.getMonth();

     

       1673
       1673
       +
                           

     

       1674
       1674
       +
                           // Set most recent date as the active period in the timeline

     

       1675
       1675
       +
                           const yearEl = document.querySelector(`.timeline-year[data-year="${year}"]`);

     

       1676
       1676
       +
                           const monthEl = document.querySelector(`.timeline-month[data-year="${year}"][data-month="${month}"]`);

     

       1677
       1677
       +
                           

     

       1678
       1678
       +
                           // Clear all active classes first

     

       1679
       1679
       +
                           document.querySelectorAll('.timeline-year.active, .timeline-month.active').forEach(el => {

     

       1680
       1680
       +
                               el.classList.remove('active');

     

       1681
       1681
       +
                           });

     

       1682
       1682
       +
                           

     

       1683
       1683
       +
                           // Add active classes to the appropriate year/month

     

       1684
       1684
       +
                           if (yearEl) {

     

       1685
       1685
       +
                               yearEl.classList.add('active');

     

       1686
       1686
       +
                               lastActiveYear = year;

     

       1687
       1687
       +
                           }

     

       1688
       1688
       +
                           if (monthEl) {

     

       1689
       1689
       +
                               monthEl.classList.add('active');

     

       1690
       1690
       +
                               lastActiveMonth = month;

     

       1691
       1691
       +
                           }

     

       1692
       1692
       +
                           

     

       1693
       1693
       +
                           // Show the month header for the most recent month

     

       1694
       1694
       +
                           document.querySelectorAll('.month-year-header').forEach(header => {

     

       1695
       1695
       +
                               header.style.visibility = 'hidden';

     

       1696
       1696
       +
                           });

     

       1697
       1697
       +
                           const recentHeader = document.querySelector(`.month-year-header[data-year="${year}"][data-month="${month}"]`);

     

       1698
       1698
       +
                           if (recentHeader) {

     

       1699
       1699
       +
                               recentHeader.style.visibility = 'visible';

     

       1700
       1700
       +
                           }

     

       1701
       1701
       +
                       }

     

       1702
       1702
       +
                       

     

       1663
       1703
        
                       // Helper function to observe all items with date attributes

     

       1664
       1704
        
                       function observeAllDateItems() {

     

       1665
       1705
        
                           // Observe all feed items for scroll tracking

     
···

       1915
       1955
        
                       linkMonthHeaders.forEach((header, index) => {

     

       1916
       1956
        
                           header.style.visibility = index === 0 ? 'visible' : 'hidden';

     

       1917
       1957
        
                       });

     

       1958
       1958
       +
                       

     

       1959
       1959
       +
                       // If we have links, set the most recent link's date as active in the timeline for the links tab

     

       1960
       1960
       +
                       if (dedupedLinks.length > 0) {

     

       1961
       1961
       +
                           const mostRecentLink = dedupedLinks[0];

     

       1962
       1962
       +
                           const linkDate = mostRecentLink.date;

     

       1963
       1963
       +
                           const linkYear = linkDate.getFullYear();

     

       1964
       1964
       +
                           const linkMonth = linkDate.getMonth();

     

       1965
       1965
       +
                           

     

       1966
       1966
       +
                           // Add a flag to remember we've set a most recent link

     

       1967
       1967
       +
                           window.mostRecentLinkSet = {

     

       1968
       1968
       +
                               year: linkYear,

     

       1969
       1969
       +
                               month: linkMonth

     

       1970
       1970
       +
                           };

     

       1971
       1971
       +
                       }

     

       1918
       1972
        
                       

     

       1919
       1973
        
                       // Process people data

     

       1920
       1974
        
                       const peopleContainer = document.querySelector('.people-container');

+2 -93

threads.json

···

       29
       29
        
             }

     

       30
       30
        
           ]

     

       31
       31
        
         },

     

       32
       32
       -
         "https://www.jonmsterling.com/2025-W15/": {

     

       33
       33
       -
           "id": "https://www.jonmsterling.com/2025-W15/",

     

       34
       34
       -
           "title": "Weeknotes 2025-W15",

     

       35
       35
       -
           "link": "https://www.jonmsterling.com/2025-W15/",

     

       36
       36
       -
           "feed_title": "Jon Sterling \u203a Weeknotes",

     

       37
       37
       -
           "references": [

     

       38
       38
       -
             {

     

       39
       39
       -
               "id": "https://www.forester-notes.org/JVIT/",

     

       40
       40
       -
               "link": "https://www.forester-notes.org/JVIT/",

     

       41
       41
       -
               "title": "Towards Forester 5.0 II: a design for canonical URLs",

     

       42
       42
       -
               "feed_title": "Forester Blog",

     

       43
       43
       -
               "in_feed": true

     

       44
       44
       -
             },

     

       45
       45
       -
             {

     

       46
       46
       -
               "id": "https://patrick.sirref.org/weekly-2025-03-31/",

     

       47
       47
       -
               "link": "https://patrick.sirref.org/weekly-2025-03-31/",

     

       48
       48
       -
               "title": "Shelter, Hazel and More!",

     

       49
       49
       -
               "feed_title": "Weeklies",

     

       50
       50
       -
               "in_feed": true

     

       51
       51
       -
             }

     

       52
       52
       -
           ],

     

       53
       53
       -
           "referenced_by": [],

     

       54
       54
       -
           "external_links": [

     

       55
       55
       -
             {

     

       56
       56
       -
               "url": "https://www.forester-notes.org/jms-011P/",

     

       57
       57
       -
               "normalized_url": "https://forester-notes.org/jms-011P",

     

       58
       58
       -
               "in_feed": false

     

       59
       59
       -
             },

     

       60
       60
       -
             {

     

       61
       61
       -
               "url": "https://git.sr.ht/~jonsterling/forester-base-theme/commit/a251f9cf19b0ff42f4553d315df5181b985c79cb",

     

       62
       62
       -
               "normalized_url": "https://git.sr.ht/~jonsterling/forester-base-theme/commit/a251f9cf19b0ff42f4553d315df5181b985c79cb",

     

       63
       63
       -
               "in_feed": false

     

       64
       64
       -
             },

     

       65
       65
       -
             {

     

       66
       66
       -
               "url": "https://topiary.tweag.io/",

     

       67
       67
       -
               "normalized_url": "https://topiary.tweag.io",

     

       68
       68
       -
               "in_feed": false

     

       69
       69
       -
             },

     

       70
       70
       -
             {

     

       71
       71
       -
               "url": "https://github.com/RedPRL/cooltt",

     

       72
       72
       -
               "normalized_url": "https://github.com/RedPRL/cooltt",

     

       73
       73
       -
               "in_feed": false

     

       74
       74
       -
             },

     

       75
       75
       -
             {

     

       76
       76
       -
               "url": "https://github.com/RedPRL/redtt",

     

       77
       77
       -
               "normalized_url": "https://github.com/RedPRL/redtt",

     

       78
       78
       -
               "in_feed": false

     

       79
       79
       -
             },

     

       80
       80
       -
             {

     

       81
       81
       -
               "url": "https://github.com/RedPRL/sml-redprl",

     

       82
       82
       -
               "normalized_url": "https://github.com/RedPRL/sml-redprl",

     

       83
       83
       -
               "in_feed": false

     

       84
       84
       -
             },

     

       85
       85
       -
             {

     

       86
       86
       -
               "url": "https://lawrencecpaulson.github.io/tag/locales",

     

       87
       87
       -
               "normalized_url": "https://lawrencecpaulson.github.io/tag/locales",

     

       88
       88
       -
               "in_feed": false

     

       89
       89
       -
             },

     

       90
       90
       -
             {

     

       91
       91
       -
               "url": "https://www21.in.tum.de/~ballarin/publications/jar2019.pdf",

     

       92
       92
       -
               "normalized_url": "https://www21.in.tum.de/~ballarin/publications/jar2019.pdf",

     

       93
       93
       -
               "in_feed": false

     

       94
       94
       -
             },

     

       95
       95
       -
             {

     

       96
       96
       -
               "url": "https://github.com/agda/agda/issues/5837",

     

       97
       97
       -
               "normalized_url": "https://github.com/agda/agda/issues/5837",

     

       98
       98
       -
               "in_feed": false

     

       99
       99
       -
             },

     

       100
       100
       -
             {

     

       101
       101
       -
               "url": "https://www.abebooks.co.uk/9789812701428/Domain-theoretic-Foundations-Functional-Programming-Streicher-9812701427/plp",

     

       102
       102
       -
               "normalized_url": "https://abebooks.co.uk/9789812701428/Domain-theoretic-Foundations-Functional-Programming-Streicher-9812701427/plp",

     

       103
       103
       -
               "in_feed": false

     

       104
       104
       -
             }

     

       105
       105
       -
           ]

     

       106
       106
       -
         },

     

       107
       32
        
         "https://mort.io/blog/coping-and-capping/": {

     

       108
       33
        
           "id": "https://mort.io/blog/coping-and-capping/",

     

       109
       34
        
           "title": "Coping and Capping",

     
···

       983
       908
        
           "link": "https://patrick.sirref.org/weekly-2025-03-31/",

     

       984
       909
        
           "feed_title": "Weeklies",

     

       985
       910
        
           "references": [],

     

       986
       986
       -
           "referenced_by": [

     

       987
       987
       -
             {

     

       988
       988
       -
               "id": "https://www.jonmsterling.com/2025-W15/",

     

       989
       989
       -
               "link": "https://www.jonmsterling.com/2025-W15/",

     

       990
       990
       -
               "title": "Weeknotes 2025-W15",

     

       991
       991
       -
               "feed_title": "Jon Sterling \u203a Weeknotes",

     

       992
       992
       -
               "in_feed": true

     

       993
       993
       -
             }

     

       994
       994
       -
           ],

     

       911
       911
       +
           "referenced_by": [],

     

       995
       912
        
           "external_links": [

     

       996
       913
        
             {

     

       997
       914
        
               "url": "https://github.com/quantifyearth/shark",

     
···

       1408
       1325
        
               "in_feed": true

     

       1409
       1326
        
             }

     

       1410
       1327
        
           ],

     

       1411
       1411
       -
           "referenced_by": [

     

       1412
       1412
       -
             {

     

       1413
       1413
       -
               "id": "https://www.jonmsterling.com/2025-W15/",

     

       1414
       1414
       -
               "link": "https://www.jonmsterling.com/2025-W15/",

     

       1415
       1415
       -
               "title": "Weeknotes 2025-W15",

     

       1416
       1416
       -
               "feed_title": "Jon Sterling \u203a Weeknotes",

     

       1417
       1417
       -
               "in_feed": true

     

       1418
       1418
       -
             }

     

       1419
       1419
       -
           ],

     

       1328
       1328
       +
           "referenced_by": [],

     

       1420
       1329
        
           "external_links": [

     

       1421
       1330
        
             {

     

       1422
       1331
        
               "url": "https://web.archive.org/",