You are viewing archived messages.
Go here to search the history.

Kartik Agaram 2021-08-11 05:46:08
Chris Knott 2021-08-11 12:18:35

Did I miss you adding networking 🤔

Kartik Agaram 2021-08-11 14:24:16

Nope! You won't be able to click on links for the foreseeable future. I'm hoping it's still useful just to bounce around between crosslinks. And search.

There can also be a port atop Linux. With networking but no avatars. That's probably a good trade-off 😄

Kartik Agaram 2021-08-12 02:32:42

Here's a release you can try out of my network-less offline-only read-only browser for FoC archives:

http://akkartik.name/mu/mu-slack-browser-20210811.img.gz (70KB)

http://akkartik.name/mu/foc-data-20210811.img.gz (16MB)

Download and gunzip both, and then run (using Qemu on Linux):

qemu-system-i386 -accel kvm -m 2G -hda mu-slack-browser-20210811.img -hdb foc-data-20210811.img

For other platforms, drop the -accel kvm. But it'll be significantly slower (5-25x, depending on what acceleration you have available)

Even on Linux, the app currently loads all 55MB in the data disk (including uncompressed avatars) on startup, which takes around 3 minutes. (Edit: interestingly, I actually have the disk load up in just 30 seconds if I drop the -accel kvm 🤔)

After that 3-minute wait, all you get at the moment is a river-of-news view that mingles all posts and comments in strict reverse chronological order. Page up, page down, that's it. I plan to implement other ways to slice and dice items by channel, post, user.

Other known issues:

  • This isn't a pure-Mu solution. I'm converting Slack archives to Mu data disk images using a Python script and a few other dependencies: https://github.com/akkartik/mu/blob/main/browse-slack/convert_slack.py
  • No search yet, though I've got misleading placeholders in the UI.
  • No message text parsing yet, so no hyphenation, no Unicode escapes, no translation of Slack :emoji:
  • ... (please report others!)

Things that are very far away: opening attachments and URLs, editing, reacji, anything that requires network access.

Does anyone have objections to publicizing these disk images more broadly? There's no DMs in them, and I know we consider the channels here to be a public record. But now it might be a lot more amenable to drive-by browsing. cc Ivan Reese Mariano Guerra

(Apologies for monopolizing this channel two days in a row. I didn't think things through with my over-excited teaser yesterday.)

Kartik Agaram 2021-08-12 04:44:11

Whoa, it's amazing how much stuff I've been missing out on within comments.

Mariano Guerra 2021-08-12 07:28:25

The 3 main channels are archived on github so I don't see a problem with this one (or if there is then I have a problem too :D)

Ivan Reese 2021-08-12 14:16:02

Yeah, I think it's fine to share the public slack discussions openly / widely.

Andreas S. 2021-08-14 07:14:56

Pretty impressive, really

Kartik Agaram 2021-08-12 02:32:42

Here's a release you can try out of my network-less offline-only read-only browser for FoC archives:

http://akkartik.name/mu/mu-slack-browser-20210811.img.gz (70KB)

http://akkartik.name/mu/foc-data-20210811.img.gz (16MB)

Download and gunzip both, and then run (using Qemu on Linux):

qemu-system-i386 -accel kvm -m 2G -hda mu-slack-browser-20210811.img -hdb foc-data-20210811.img

For other platforms, drop the -accel kvm. But it'll be significantly slower (5-25x, depending on what acceleration you have available)

Even on Linux, the app currently loads all 55MB in the data disk (including uncompressed avatars) on startup, which takes around 3 minutes. (Edit: interestingly, I actually have the disk load up in just 30 seconds if I drop the -accel kvm 🤔)

After that 3-minute wait, all you get at the moment is a river-of-news view that mingles all posts and comments in strict reverse chronological order. Page up, page down, that's it. I plan to implement other ways to slice and dice items by channel, post, user.

Other known issues:

  • This isn't a pure-Mu solution. I'm converting Slack archives to Mu data disk images using a Python script and a few other dependencies: https://github.com/akkartik/mu/blob/main/browse-slack/convert_slack.py
  • No search yet, though I've got misleading placeholders in the UI.
  • No message text parsing yet, so no hyphenation, no Unicode escapes, no translation of Slack :emoji:
  • ... (please report others!)

Things that are very far away: opening attachments and URLs, editing, reacji, anything that requires network access.

Does anyone have objections to publicizing these disk images more broadly? There's no DMs in them, and I know we consider the channels here to be a public record. But now it might be a lot more amenable to drive-by browsing. cc Ivan Reese Mariano Guerra

(Apologies for monopolizing this channel two days in a row. I didn't think things through with my over-excited teaser yesterday.)

Robin Allison 2021-08-14 06:56:25

I'd like to make a general point: Arbitrary mathematical statements formulated symbolically can be formulated with concrete dynamic variables instead (by which I mean concrete values you can change and whose instances are all kept in sync). Here is an example of this with the pythagorean theorem. https://www.youtube.com/watch?v=QemB5t94slc Normally it would read "If a,b, and c are the lengths of the two legs and the hypotenuse respectively of a right triangle then a^2+b^2=c^2". However, this is equivalent to an expression with dynamic variables, as illustrated in the video. Any instance of the general theorem can be achieved by altering the values of the dynamic variables to that particular instance. Moreover, no matter how the values of the formulation with dynamic variables is altered the resulting statement will always be an instance of the pythagorean theorem because the values at different locations are always kept in sync. Thus, insofar as the two formulations have the same instances, the two are equivalent. (also, modulo the fact that the present scrubbing mechanism can only produce integers).

This is part of a broader set of ideas I'm exploring. I'm trying to develop a theory of what I'm terming "formal dynamic mathematics." By dynamic mathematics I mean mathematics employing dynamic variables, and which aren't necessarily "mathematical objects" (any sort of set) but could be interactive visual elements such as a line segment which you can move around and whose length you can alter or metamathematical objects such as variable names. These sorts of variables abound in geogebra, bret victors work, apparatus (Toby Schachman), and pane (Joshua Horowitz), among other 'live' systems. I think we would benefit from a more systematic understanding of the interface primitives that go into them.

We can roughly analyze these applications in terms of three primitives: transclusion, evaluation, and varriers. By transclusion I mean the live copying of the contents of one part of a page into another part of the page. Having a transclusion from one region to another and another back again ensures that those two regions will always have the same value, effectively yielding a variable without a name or a value. Evaluation is a relation between different regions of a page where the values in different regions of the page are operated on and displayed in another location. Finally, varriers are primitives having values and modes of interaction. A scrubbable number is an example of a varrier. (apologies for the neologism; suggestions for better words or similar vocabulary is welcome)

Just as normal formal mathematics is built out of its own primitives (sequences of symbols and rules of inference) formal dynamic mathematics is built out of the above primitives. Inferences rules can be formalized as evaluation schemas so constructions in these systems are proofs.

Although this kind of math could be used to design end user programming systems, I'm mostly interested in its application to math itself, as an extension of the language of math at a fundamental level. An idea I've been exploring this year substantially has been how to develop an entirely visual language (save for the logical connectives of propositional and predicate calculus) for vector algebra, without any symbols, and in particular to be able to state and prove the pythagorean theorem from axioms. (This problem was pretty much posed by Hamish Todd about a year ago). Dynamic variables and varriers (for visual vectors) easily let you do away with symbolic variables. This reduces the problem to devising a visualization for concrete static terms built with functions. We can easily visualize terms like (1,2)+(3,5), and proj_{(1,1)}(4,5) but visualizations for more complex terms generally seem ad hoc. I think there is a solution here, but it's a matter of understanding why there isn't an ideal solution, and I don't understand that well enough at this point to share.