enricozb

This is the video source of the gif at the top of the article [0].

I was pretty interested in Penrose when I first saw it but I still haven't seen a "cool" example of its use. Either something that's easy in Penrose but hard in every other visualization tool, or an example of a visualization in Penrose that elucidates some deeper mathematical relationship between the objects being shown.

[0] https://vimeo.com/416822487

It looks like you're right. I guess I don't really understand then why we can't just log in as root in vanilla iOS

Since ML outputs are usually "fuzzy", how does one check that the output is actually correct when using a technique like this in the field?

It doesn't install OpenSSH by default, but it does set up a root user with a default password "alpine". It's recommended that you change this.

Would love to see an FP language on there, preferably OCaml

I can already imagine trying to debug a templated type error with code that was generated at compile time...

Both are beautiful in their own ways. I think ReasonML, or even SML or OCaml might be a gentler introduction since they let you write imperative code (more closely to what you probably write already) whenever you need to.

For example, I think there is a gradient from OCaml > Clojure > Haskell about using mutable data structures in your code, from Encourage > Discourage > Disallow. I think learning Haskell as your first FP might turn you off given how strict it is in this regard. So using that as a line of reasoning, using OCaml or ReasonML might be best since it lends an imperative hand whenever you need it, and lets you explore all of the amazing things FP has to offer.

Is it still the case that when you have an error in your script (and aren't using RStudio) that you don't get the line number of the error, you just get a traceback?

I use Youtube for music, so I usually have a tab open for prolonged time. However, I also waste some time on Youtube by randomly opening a tab. Is there any way you plan on handling this use case?

One of my favorites:

Greerg: #123321

I have never been able to get EPUBs to reliably work on remarkable. My solution is to convert them to PDFs.

Awesome. I've been looking for more Lean resources outside of Theorem Proving in Lean [1].

[1]: https://leanprover.github.io/theorem_proving_in_lean/

> no known physical laws seem to require a single direction.

What would a physical law that required a single direction look like?

If you want to "overload" a function. Do

    def area(shape):
      return shape.area()

and implement it appropriately in your type.

It hurts my heart how conflicted I am about this device. The hardware _is_ there. I love using the original reMarkable tablet _when it works_. But damn there are some stupid software decisions, alongside some absolutely genius ones. (Disclaimer: I've had the original reMarkable tablet for 3 months now) Here's a summary of my experience with it:

- It's sometimes unstable, and crashes while I draw. Not super often but maybe 4 or 5 times a week. I don't lose any data other than the last ~5-10 strokes.

- There is a notebook called Quick Sheets that is permanently there, even if I try to remove it's metadata over SSH. It gets generated on boot. No idea why this is here.

- You can SSH in, and there's a good hacker community around the tablet. A lot of cool open source software is written for it.

- Putting a file on the device for the first time, after doing the same on a kindle for years, is an adventure to say the least. There is no calibre plugin for it that I've found.

- I have never been able to use EPUBs properly on this tablet, a lot of my books just crash it. I have to convert them to PDF first on calibre. So highlighting is just markup on the PDF and not really selecting any text, but you can write directly on the book with notes.

- The first time I opened an EPUB, it took a while (10s) to load. When I tried to change the font of the EPUB on the reMarkable, it just stayed on the loading icon for hours, and I gave up on EPUBs then, and resorted to PDFs.

- There is no dictionary on the EPUB reader. I miss this feature a lot. And even if there were, I wouldn't be able to use it because I have to convert my EPUBs to PDF.

- Metadata for EPUBs or PDFs isn't visible, only the raw filenames. So no sorting by author, genre, etc.

- drawing and marking up is phenomenal, as is reading on such a huge screen. I absolutely love reading and journaling on this tablet.

- I have never succeeded in exporting my notebooks or marked up PDFs using the built in software after marking up or writing in 100+ pages, I have to use some community written software instead.

- It's $500 total after pen and cover.

- There is no backlight.

- OCR is done in the cloud, and not on the device.

- The iOS companion app is goofy, a lot of the navigation within the app seems to be done in a hacky way, instead of using the usual iOS SDK components. (They segment screen portions for scrolling on pages and for navigating the app, and it leads to just the most bizarre behavior).

I want to love this tablet. And all we need is a software update. The hardware was almost perfect, and now with USB-C, a magnet on the pen, and an eraser, the hardware is even closer to being perfect (I think the only thing left is a backlight).

Pretty sure you can attach to an already attached tmux session as well, which I believe has the same behavior that you’re describing. I’ve never used screen, is what you’re describing different than what I’m talking about?

Hopefully as theorem provers improve and become more expressive, we can begin to state these theorems and even formalize proofs of them, letting a computer verify the proof for us. Check out Lean[1] if this sounds interesting to you.

[1]: https://leanprover.github.io/

Check out Kakoune[1] for a different take on an editor’s scripting language. It offloads as much as possible to existing Unix tools such as bash, sort, fmt, etc. It uses a clever system of string substitutions that’s a bit unintuitive at first, but not too difficult to grasp quickly. I spent two weeks trying to fix a bug in a Vim plugin that ended up being a 3 line change. After that I felt like I barely understood just a small section of vimscript.

I ended up switching to Kakoune after trying it for a bit because I realized that in the two weeks of me exploring it I had entirely understood it’s “scripting language”, or at the very least understood how to use the onboard docs to write any plugin I wanted to.

[1]: https://github.com/mawww/kakoune

Deepcell[1] is a framework I worked on for a bit during my undergrad. It can do cell segmentation & tracking for different imaging types.

[1]: https://github.com/vanvalenlab/deepcell-tf/blob/master/READM...

I still sometimes have the A<esc> anti-pattern. It's slowly been disappearing since I added gl. The kakoune keybindings were designed with a lot of thought behind them. They seem extremely natural.

Also, I meant to say that the my replacements for 0, $, gg, and G are gh, gl, gk, gj. 'g' for 'go' and 'hjkl' for the standard up, down, left, or right.

Using kakoune for the first time made me understand how much better the vim keybindings could be. I switched the weird begin & end of line navigations (0 and $) to (gl and gr) as they are in Kakoune, and I also added the move view (v* in kakoune) commands to vim.

Also my goodness having built-in multiple cursors is fantastic. Kakoune multiple cursors is much much better than the vim plugins for multiple cursors.

As other people have said though, there are some plugins that have yet to be ported to kakoune. iirc smooth scrolling (comfortable-motion) and vim-wiki to name the ones that come to my mind.

Could this be used on a local network? I have a pretty beefy PC but I like the comfort of sitting outside with my chromebook. Is there any way to host this service myself, so it doesn't have to go through any servers first?