e0qdk

It’s not a GUI library, but Jupyter was pretty much made for the kind of mathematical/scientific exploratory programming you’re interested in doing. It’s not the right tool for making finished products, but is intended for creating lab notebooks that contain executable code snippets, formatted text, and visual output together. Given your background experience and the libraries you like, it seems like it’d be right up your alley.

Can Z3 account for lost bits? Did it come up with just one solution?

It gave me just one solution the way I asked for it. With additional constraints added to exclude the original solution, it also gives me a second solution – but the solution it produces is peculiar to my implementation and does not match your implementation. If you implemented exactly how the bits are supposed to end up in the result, you could probably find any other solutions that exist correctly, but I just did it in a quick and dirty way.

This is (with a little clean up) what my code looked like:

#!/usr/bin/env python3

import z3

rand1 = 0.38203435111790895
rand2 = 0.5012949781958014
rand3 = 0.5278898433316499
rand4 = 0.5114834443666041

def xoshiro128ss(a,b,c,d):
    t = 0xFFFFFFFF & (b << 9)
    r = 0xFFFFFFFF & (b * 5)
    r = 0xFFFFFFFF & ((r << 7 | r >> 25) * 9)
    c = 0xFFFFFFFF & (c ^ a)
    d = 0xFFFFFFFF & (d ^ b)
    b = 0xFFFFFFFF & (b ^ c)
    a = 0xFFFFFFFF & (a ^ d)
    c = 0xFFFFFFFF & (c ^ t)
    d = 0xFFFFFFFF & (d << 11 | d >> 21)
    return r, (a, b, c, d)

a,b,c,d = z3.BitVecs("a b c d", 64)
nodiv_rand1, state = xoshiro128ss(a,b,c,d)
nodiv_rand2, state = xoshiro128ss(*state)
nodiv_rand3, state = xoshiro128ss(*state)
nodiv_rand4, state = xoshiro128ss(*state)

z3.solve(a >= 0, b >= 0, c >= 0, d >= 0,
  nodiv_rand1 == int(rand1*4294967296),
  nodiv_rand2 == int(rand2*4294967296),
  nodiv_rand3 == int(rand3*4294967296),
  nodiv_rand4 == int(rand4*4294967296)
  )

I never heard about Z3

If you’re not familiar with SMT solvers, they are a useful tool to have in your toolbox. Here are some links that may be of interest:

• https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
• https://en.wikipedia.org/wiki/Z3_Theorem_Prover

Edit: Trying to fix formatting differences between kbin and lemmy
Edit 2: Spoiler tags and code blocks don’t seem to play well together. I’ve got it mostly working on Lemmy (where I’m guessing most people will see the comment), but I don’t think I can fix it on kbin.

If I understand the problem correctly, this is the solution:

I solved it with Z3. Took less than a second of computer time, and about an hour of my time – mostly spent trying to remember how the heck to use Z3 and then a little time debugging my initial program.

What I’d do is set up a simple website that uses a little JavaScript to rewrite the date and time into the page and periodically refresh an image under/next to it. Size the image to fit the remaining free space of however you set up the iPad, and then you can stick anything you want there (pictures/reminder text/whatever) with your favorite image editor. Upload a new image to the server when you want to change the note. The idea with an image is that it’s just really easy to do and keeps the amount of effort to redo layout to a minimum – just drag stuff around in your image editor and you’ll know it’ll all fit as expected as long as you don’t change the resolution (instead of needing to muck around with CSS and maybe breaking something if you can’t see the device to check that it displays correctly).

There’s a couple issues to watch out for – e.g. what happens if the internet connection/server goes down, screen burn-in, keeping the browser from being closed/switched to another page, keeping it powered, etc. that might or might not matter depending on your particular circumstances. If you need to fix all that for your circumstances, it might be more trouble than just buying something purpose built… but getting a first pass DIY version working is trivial if you’re comfortable hosting a website.

Edit: If some sample code that you can use as a starting point would be helpful, let me know.

Any ways to get around the download failing

I did this incredibly stupid procedure with Firefox yesterday as a workaround for a failing Google Takeout download:

• backup the .part file from the failed download
• restart the download (careful – if you didn’t move/back it up, it will be deleted and you will have to download the whole thing again; found this out the hard way on a 50GB+ file… that failed again)
• immediately pause the new download after it starts writing to disk
• replace the new .part file with the old .part file from earlier (or – see [1] below)
• Firefox might not show progress for a long time, but will eventually continue the download (I saw it reading the file back from disk with iotop so I just let it run)
• sanity check that you actually got the whole thing and that it is usable (in my case, I knew a hash for the file)

[1] You can actually replace the new .part file with anything that has the same size in bytes as the old file – I replaced it with a file full of zeros and manually merged the end onto the original .part file with a tiny custom python script since I had already moved the incomplete file to other media before realizing I could try this. (In my case, the incomplete file would still have been useful even with the last ~1MB cut off.)

There are probably better options in most cases – like Thunderbird for mailbox as other people suggested, or rclone for getting stuff from Drive – but if you need to get Takeout to work and the download keeps failing this may be another option to try.

A vote on kbin/lemmy is closer to a retweet than to a vote on reddit in terms of its potential impact on folks. You are publicly saying you support/do not support a post by voting on it (which might be taken as publicly thanking someone with an upvote or publicly saying fuck you with a downvote in some contexts); that can be a workable system, but it’s surprising if you’re coming from reddit where basically no one but the admins (and whoever they told/sold the data to) actually knows what you voted up/down.

Hell, consider all the drama around “YOU DOWNVOTED ME!!” / “No I didn’t!” BS that was so common even when it was just suspected – now it can be confirmed (again, for better or worse), for kbin users. I was on reddit for a long time and just thinking about that crap makes me feel tired… -.- Downvoting on kbin is potentially picking a fight every time. The end result is that I’ve basically never downvoted anything except some spam bots. I don’t need that shit in my life again – even for some of the posts that I think really should be downvoted, I’m just ignoring now. (Not getting into it further. Don’t ask. I won’t respond.)

If your IRL identity is associated with your account (or can be figured out eventually…), upvoting something really spicy could also end up causing you the same kind of drama IRL as retweeting or commenting strongly on the post – e.g. job loss, loss of business, targeted harassment/violence campaigns, loss of friends/romantic partners, etc…

I really don’t need more drama in my life, so I’m a bit more mindful of how I’m voting (for better or worse) and some stuff I probably would’ve voted on before, I am just leaving alone now.

Harassment, mostly.

Yeah, I had a mixed reaction to finding that out a while ago, but I’m kind of just rolling with it for now. Votes are just simply NOT private on here, for better or worse. My feeling right now is that it’s sort of positive from a community feel perspective, but I’m also avoiding interacting with a lot of subjects I consider more controversial.

Probably we’ll end up developing a culture of either lots of alts used simultaneously, short lived accounts with regular name changes, or both as people become more aware of this. Either that or people will just say “Fuck it. You really want to see all the weird porn I like and my political preferences and what not? Don’t blame me if you regret looking!” :p

Anyone can see any upvote from federated users via kbin – for example, the upvotes on the comment this is a reply to can be seen here: https://kbin.social/m/[email protected]/t/616970/If-you-can-create-a-Lemmy-instance-and-federate-you/comment/3491191/favourites

That may not be complete or consistent though given the way federation works.

Downvotes from lemmy do not show up. (Not sure why not; haven’t dug into it.) Only downvotes from kbin members are shown on kbin. Also unclear to me if downvotes between different kbin/mbin instances show up or if it’s the local instance only. (I’ve only noticed local downvotes, but haven’t really been looking.)

Rule 9 from Agans’s Debugging: If you didn’t fix it, it ain’t fixed

Intermittent problems are the worst…

I met a traveller from an antique land
Who said: Two vast and trunkless legs of stone
Stand in the desart. Near them, on the sand,
Half sunk, a shattered visage lies, whose frown,
And wrinkled lip, and sneer of cold command,
Tell that its sculptor well those passions read
Which yet survive, stamped on these lifeless things,
The hand that mocked them and the heart that fed:
And on the pedestal these words appear:
“My name is Ozymandias, king of kings:
Look on my works, ye Mighty, and despair!”
Nothing beside remains. Round the decay
Of that colossal wreck, boundless and bare
The lone and level sands stretch far away.

-- Percy Shelley, “Ozymandias”, 1819 edition
(copied from Wikipedia)

I’ve used Wireshark when I want to inspect the traffic going through my computer. I’ve found it particularly handy for debugging my own networking code. I’ve also used netstat to see active connections and programs listening for traffic when I don’t care about the packet contents specifically.

I think it’s probably an Indian English-ism. It’s understandable but sounds weird to speakers of American English (and maybe other English dialects).

A more natural sounding title (to an American English speaker) would use “Microsoft is making” or “Microsoft is planning to make” rather than “Microsoft might want to be making”.

With that said, can I possibly only allow traffic to and fro from the proxy through my firewall?

Yes. That is what I suggested. If you configure the firewall to only allow traffic to/from the specific IP and port combination of your proxy, other traffic will be blocked.

I should be able to (in theory) inspect traffic too, although I don’t know how far that will take me.

You can do content filtering via a proxy like that, yes. A similar sort of configuration is used on school computers to do things like block adult content, with varying degrees of success. Some ad-blocking techniques work on similar principles.

If I understood your question correctly, you’d run the proxy application (which might be Squid or Apache or some other program) either on the host computer outside the VM or elsewhere on your network. (I’m not well versed on all the ins and outs of setting Firefox up to communicate through a proxy; I just know it can be done.) The proxy would listen for incoming traffic on a specific port you configure. You then tell Firefox (in its network settings) to communicate with the specific IP and port of the proxy instead of talking to web servers directly.

To prevent other programs from communicating, you’d firewall off the VM with iptables (or maybe ufw or something else depending on what you use on your system). You’d set it to drop all traffic going to/from the VM’s network except packets going to or coming from the specific IP/port combinations you want to allow.

This isn’t a bulletproof way to block other apps from talking to the internet – anything that knows about the proxy (or which can hijack/manipulate a program like Firefox that you’ve told about the proxy) could communicate with web servers via the proxy, but depending on your specific concerns it may be good enough.

You could try configuring Firefox to access the internet through a proxy and then block the VM off from everything except the proxy and your network mount with a firewall (outside the VM).

This is totally going to turn into another JBIG2 lossy compression clusterfuck isn’t it…

For those who are unfamiliar, JBIG2 is a compression standard that has a dubious reputation for replacing characters incorrectly in scanned documents (so 6 could become an 8, for example) leading to potentially serious issues when scanning things like medical and legal documents, construction blueprints, etc.

I ran my own email server about 10-ish years ago for a while on a Linode using Postfix and Dovecot similar to what others have mentioned. Took some effort to prevent GMail from just flagging everything I sent as spam, but I was eventually able to do it. I remember having to configure something particular with DNS records. (An SPF TXT record, probably?)

I didn’t end up using it very much and shut it down after a couple years, but it was a good exercise and I learned a lot from doing it.