I write code and play games and stuff. My old username from reddit and HN was already taken and I couldn’t think of anything else I wanted to be called so I just picked some random characters like this:

>>> import random
>>> ''.join([random.choice("abcdefghijklmnopqrstuvwxyz0123456789") for x in range(5)])
'e0qdk'

My avatar is a quick doodle made in KolourPaint. I might replace it later. Maybe.

日本語が少し分かるけど、下手です。

Alt: e0qdk@reddthat.com

  • 1 Post
  • 12 Comments
Joined 1 year ago
cake
Cake day: September 22nd, 2023

help-circle
  • 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:

    solver code
    #!/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:

    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:

    solution

    a = 2299200278
    b = 2929959606
    c = 2585800174
    d = 3584110397

    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.



  • Didn’t the GDPR have a data portability rule requiring that sites provide users the ability to easily export their own data? Does that not apply to Lemmy for some reason – or, am I misremembering it? (I remember account data download being a big deal a while back on reddit, but it’s been a few years…)





  • 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.


  • Haven’t used that particular library, but have written libraries that do similar sorts of things and have played with a few other similar libraries in C++ and Haskell. I’ve taken a quick glance at the documentation here, but since I don’t know this library specifically apologizes in advance if I make a mistake.

    For OneOrMore(Word(alphanums)) + OneOrMore(Char(printables)) it looks it matches as many alphanum Words as it can (whitespace sequences being an acceptable separator between tokens by default) and when it hits ( it cannot continue with that so tries to match the next expression in the sequence. (i.e. OneOrMore(Char(printables)))

    The documentation says:

    Char - a convenience form of Word that will match just a single character from a string of matching characters

    Presumably, that means it will not group the characters together, which is why you get individual character matches after that point for all the remaining non-whitespace characters. (Your result also seems to imply there was a semicolon at the end of your input?)

    For OneOrMore(Word(alphanums)) + OneOrMore(Char(string.punctuation)) it looks like it cannot match further than ( since 1 is not a punctuation character; so, you got the tokens for the parts of the string that matched. (If you chained the parser expression with something like + Word(alphanum) I’d expect you’d get another token [i.e. "1"] added onto the end of your result.) You may eventually want StringEnd/LineEnd or something like that – I’d expect they’d fail the parser expression if there’s unconsumed input (for error detection), but again, haven’t used this specific library, so it may work different than I expect.

    There appears to be a Combine class you can use to join string results together; that might be useful for future reference.

    i was trying to parse a string with pyparsing so all the words were separated from the punctuation signs

    Have not tested it (since I don’t have a copy of the library installed anywhere and can’t set up an environment for it easily right now) but perhaps something like OneOrMore(Word(alphanums)|Char(string.punctuation)) would be more like what you are looking for?