unison VS logical_verification_2020

If you look at the release notes you can see that some versions say they are protocol compatible with prior X.Y version release

https://github.com/bcpierce00/unison/releases

You might want to try Unison: https://github.com/bcpierce00/unison

I highly recommend Unison (https://github.com/bcpierce00/unison)

It allows you to sync between 2 machines (bi-directional) over TCP or SSH.

Note that TCP way is not encrypted, you may use wireguard as transport layer encryption for that purpose...

You can use an external application to copy if file size is larger than an arbitrary number. (Eg: use rsync for files > 1gb)

The iOS app only syncs via iCloud or Obsidian Sync. I was in a similar situation (wanted to sync to Linux PCs and iPhone without paying for Sync), but I do have one always on Mac, so I set up a script that runs every minute, syncing my vault on iCloud with an identical vault on Synology Drive. My script basically just runs Unison once every few minutes to keep the two vaults in sync.

Unison is another alternative. I use it to synchronize my music with a Samba share and an usb stick, works great.

Unison

I've tested many file synchronization. I rely via scripts on Unison, originally authored by the computer scientist Benjamin Pierce, and now decades of tweaking by a strong open source community.

https://github.com/bcpierce00/unison

I'd love to see Darke Files get everything right that Unison gets right, that nearly all commercial projects get wrong, through a blend of arrogance and ignorance:

* Meta data. It takes a lot to insure that two copies of a MacOS file appear identical to a user. There used to be a test suite on the web that embarrassed everybody.

* Atomic folders such as ".git" or an application bundle. A prototypical example is a MacOS disk image, supported by a folder of many small files. This helps minimize incremental backup and transfer. Unison lets you specify the conflict resolution at the folder level, all-or-nothing decide which copy or fix it.

* Symbolic links. This is wildly complicated by users, sure they're right, who want special handling to hack features into sync software that isn't there. A symbolic link is just a file, with correct use the responsibility of the user. You wouldn't want sync software stopping to view your porn, right? They're just files, not the sync software's business.

I use Dropbox for various purposes because I need to, but they bungle more of this than one would expect. For example, a typical MacOS application bundle can have internal symbolic links a typical user never notices, pointing the "current" version of resources to a versioned folder. Last I checked, Dropbox expands the symbolic link into a redundant copy, wasting space without kneecapping the app.

One could go on...

I've been using Unison [1] to sync two and more computers for years. I can't recommend it enough.

[1]: https://github.com/bcpierce00/unison

heh, I like their syllabus format (linked from the first page of the PDF): https://lean-forward.github.io/logical-verification/2020/

also, to save one the trouble of url surgery here is the actual GH repo which contains what is labeled a "tablet" version of the PDF along with solutions exercises: https://github.com/blanchette/logical_verification_2020 (unlicensed)

https://github.com/blanchette/logical_verification_2020/raw/...

Benjamin Pierce: Backtracking Generators for Random Testing

A recent book in the same vein: The Hitchhiker's Guide to Logical Verification

https://github.com/blanchette/logical_verification_2020

This is a tipping point work making the case that type theory is like a musician reading sheet music. Sure, the Beatles couldn't, but... Anyone developing a new programming language should understand languages at the level of Lean, even if the common uses of their constructs aren't theorem proving. The analogies are mind-blowing. Monadic parsing is the same thing as meta-programming tactics? I'm still wrapping my head arond that one.