Cambridge
I am an Associate Professor in Logical Foundations and Formal Methods at University of Cambridge in the Department of Computer Science and Technology.
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.
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). >
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?
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:
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
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 > * > *) >
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
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?
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) >
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. >