~jonsterling

Cambridge

http://www.jonmsterling.com/

I am an Associate Professor in Logical Foundations and Formal Methods at University of Cambridge in the Department of Computer Science and Technology.

~jonsterling/forester-discuss

Last active 6 days ago

~jonsterling/forester-devel

Last active 12 days ago

~jonsterling/public-inbox

Last active 6 months ago

~jonsterling/forester-announce

Last active 1 year, 3 months ago
View more

Recent activity

Re: Regression: import hides diagnostic errors 12 days ago

From Jon Sterling to ~jonsterling/forester-devel

On Thu, Nov 21, 2024, at 12:30 PM, Nick Hu wrote:
> (Apologies if you get multiple copies of this bug report, I tried
> sending it directly to ~jonsterling/forester@todo.sr.ht but for whatever
> reason that didn't work.)


Hi Nick,

Can you please open a ticket using the web interface here? 
https://todo.sr.ht/~jonsterling/forester.

I will have to investigate a bit to determine the correct way to 
fix the bug you have identified.

Re: Handling notation 20 days ago

From Jon Sterling to ~jonsterling/forester-discuss

On 12 Nov 2024, at 16:37, David Jaz Myers wrote:

> Hi all,
>
> I've recently started using forester and I'm really enjoying the
> experience already. I will be using forester for all my work on my
> current grant at Topos, which Owen Lynch is also on, so I hope to get
> a lot of use out of it in the near future. I really appreciate all
> your work on this wonderful tool.
>
> One thing that has caused me issues, however, is *notation*. I'd like
> to say what I've been experiencing, and throw out some ideas (with no
> knowledge of how impractical they may be to actually implement).
>

Re: [PATCH v2] LaTeX pipeline: use lualatex, better dvisvgm options 20 days ago

From Jon Sterling to ~jonsterling/forester-devel

On 13 Nov 2024, at 11:01, Nick Hu wrote:

> Whoops, I didn't test this thoroughly enough and the changes to the
> LaTeX template are completely busted.
>
> I'm still trying to get `standalone` fixed upstream, but I wonder if
> there are any better ways.
> Going through PDF does seem to work, but I'm not sure dvisvgm pdf 
> input
> is necessarily a good option, e.g. see 
> https://github.com/mgieseki/dvisvgm/issues/265
>
> Another option might be to abandon the `standalone` package; is there
> any appetite for that?

Re: [PATCH] LSP server based on Asai LSP a month ago

From Jon Sterling to ~jonsterling/forester-devel

On 30 Oct 2024, at 12:36, Kento Okura wrote:

> Capabilities:
> - Diagnostics (only parse errors at the momment)
> - DocumentSync
> - Hover
> - Inlay hints for tree addresses
> - Go to definition for imports. For transcludes, see
>  https://todo.sr.ht/~jonsterling/forester/109
> - Completion for addresses. For completion of unit paths, need to
>   investigate how to use yuujinchou's get_visible function:
>  https://ocaml.org/p/yuujinchou/5.2.0/doc/Yuujinchou/Scope/module-type-S/index.html#val-get_visible
>
> New dependencies:

Re: Additional .sty files in assets broken? a month ago

From Jon Sterling to ~jonsterling/forester-discuss

[Forgot to reply-all! Also added a paragraph to my message.] 

Very sorry about this! I should have documented it, will try to do
better in the future.

We are still considering how best to deal with 
build assets in a way that balances user expectations 
with the need to keep builds relatively independent from 
their environment.

Currently the method we suggest for dealing with this is to
inline your .sty file into a macro and then use that macro. This 
is not a perfect solution because sometimes LaTeX behaves 
differently in a .sty file vs. in a .tex file, but I will be very happy to

Re: [PATCH ocaml-forester] Add license and copyright to each source file a month ago

From Jon Sterling to ~jonsterling/forester-devel

>>
>
> Looks good to me.
>
> I will be annotating the LSP files like this:
>
> (*
>  * SPDX-FileCopyrightText: 2024 The Forester Project Contributors AND 
> The RedPRL Development Team
>  *
>  * SPDX-License-Identifier: GPL-3.0-or-later AND Apache-2.0
>  *
>  *)
>

Re: Question re: copyright notices in free software source code a month ago

From Jon Sterling to ~sircmpwn/public-inbox

Many thanks for your input!
Jon


> On Oct 26, 2024, at 12:36 PM, Drew DeVault <sir@cmpwn.com> wrote:
> 
> The simplest answer is stick the text of the GPL in a file called
> COPYING and move on. If you care to put in more effort, you can check
> out reuse:
> 
> https://reuse.software
> 
> On Sat Oct 26, 2024 at 11:34 AM CEST, Jon Sterling wrote:
>> P.S. (If you have time:) I have read your blog post arguing against CLAs

Question re: copyright notices in free software source code a month ago

From Jon Sterling to ~sircmpwn/public-inbox

Dear Drew,

I am the maintainer of a free software project called Forester 
(https://sr.ht/~jonsterling/forester/), which is distributed under GPL. 
However, it came to my attention that GPL requires a copyright notice to 
appear somewhere and we had none in our repository.

This got me wondering what the right way to handle this is, and I 
figured you have an expert opinion based on some of your blog posts that 
I have read. The questions are:

1. Should copyright be explicitly attributed to each individual 
contributor? Or to "The Contributors" as a whole? What are the legal 
implications of the latter, if any?

Re: Low-brow federation is working... a month ago

From Jon Sterling to ~jonsterling/forester-devel

On 25 Oct 2024, at 15:47, Nick Hu wrote:

> Right, the issue is that forester-notes.org doesn't listen on port
> 443, so if you explicitly go to https://forester-notes.org nothing
> happens (note the https:// part is important here).
> You can observe this with the following:
>
> ❯ curl -v https://forester-notes.org
> * Host forester-notes.org:443 was resolved.
> * IPv6: (none)
> * IPv4: 216.40.34.41
> *   Trying 216.40.34.41:443... (hangs)
>

Re: Low-brow federation is working... a month ago

From Jon Sterling to ~jonsterling/forester-devel

On 24 Oct 2024, at 13:17, Nick Hu wrote:

> On Thu Oct 24, 2024 at 12:14 PM BST, Jon Sterling wrote:
>> Well, I suppose this may not be the first time that a newly minuted
>> domain takes a while to propagate into people's DNS caches.
>
> Ah, I realised what was happening. I am actually resolving the domain
> (to 216.40.34.41), but when I openened the link in Firefox it sent me 
> to
> https://forester-notes.org/ which does not seem to redirect to the www
> subdomain.
> The www subdomain resolves to a (different) sr.ht IP, and works as 
> intended.
>