<awygle>
whitequark: this is the kind of question that gets me in trouble, but... how separable is the GUI platform abstraction stuff you've done over the last 3 days or so from the solvespace codebase?
<awygle>
yeah i hit that too but like.. oh well lol. i don't even know how to solvespace so i sort of assumed i was asking for it
<whitequark>
q3k: i don't implement any of the ui elements that are supposed to be "native" yet
<whitequark>
you probably hit a code path that displays a message box
<whitequark>
it's very easy
<whitequark>
the reason i don't implement them is because modern html/js is a fucking hellscape and i hate every single character in the trash fire called webpack
<q3k>
yeah, this was a misplaced constraint
<q3k>
>webpack
<q3k>
so sorry
<whitequark>
i installed a react-create-app boilerplate creation thing and it pulled in 1100 modules.
<q3k>
yes
<q3k>
it's a shitshow
<whitequark>
i added a theme with menus and it pulled in TWO HUNDRED MORE
<q3k>
i touched js/ts for a while
<whitequark>
WHAT THE FUCK IS THIS SHIT
<q3k>
never again
<whitequark>
who the fuck considers this acceptable
<q3k>
people wo migrated from php
<q3k>
*who
<whitequark>
i started with php
<q3k>
so did I
<whitequark>
literally anything is better than this
<q3k>
yep
<q3k>
i remember trying to pack (i'm not calling this building) my first '''modern''' js project using, well makefiles
<q3k>
no fucking way
<whitequark>
hahahahaha
<q3k>
and then you use monstrosities like webpack
<awygle>
i've never really done much in JS-land, and i'm willing to take everyone's word for it that it's terrible, but i admit to some conflicted feelings on the matter. if each of those 1100 modules was well-scoped, well-written and reusable i would be delighted by them existing (but i'm sure they aren't and aren't and aren't)
<q3k>
where literally just running webpack for your shity ts codebase to generate a .js takes longer than doing 'go build' for entire fucking docker, including pulling deps from http
<q3k>
it uses execve instead of execve(shell, ...)
<pie__>
there was a scandal about this at some point
<jn__>
srsly, this is file I/O! grrr.
<q3k>
yes
<q3k>
fuck these people
<q3k>
seriously
<pie__>
haha
<awygle>
whoof. okay not getting sucked into techbashing no matter how well justified.
<pie__>
i always think what if some poor noob coded this
<q3k>
no, i don't usually care for languages
<rqou>
whitequark: i get instant crashes when tapping any of the buttons on the left on firefox beta on Android (yes yes I'm a weirdo)
<q3k>
but js deserves _all_ of htis
<q3k>
as an exception
<whitequark>
rqou: that is entirely expected
<awygle>
q3k: sure, but i don't deserve how it makes me feel afterwards
<awygle>
so i tap out
<pie__>
so i guess the solution is to review your imports??
<whitequark>
i tested this on "whatever browsers were on my machine"
<q3k>
awygle: fair enough, i'm really not proud of this either
<pie__>
also something about reputable library authors but...?
<whitequark>
pie__: good luck reviewing 1300+ webpack imports
<pie__>
whitequark, yeah i dont know what to do about this
<whitequark>
i would have better luck reviewing the entirety of qt
<awygle>
something something larger culture of nobody caring about security or efficiency
<whitequark>
because by the time i'm done, at most 20% of qt would be rewritten
<whitequark>
as opposed to 100% of webpack deps
<awygle>
facebook (react is facebook right?) could review them all but doesn't care because they don't need to care
<q3k>
facebook probably doens't pull in any 3rd party deps without review anyway
<whitequark>
well to be fair, most of that shit is compile-time dependencies
<pie__>
otoh with sometihng that has a type system i suppose you could make some automated metrics for IO code and stuff
<whitequark>
so the worst thing they can do is pwn developer machines
<whitequark>
wait
<pie__>
i think i read something about people owrking on trawling rust for unsafes
<whitequark>
that isn't any better
<q3k>
whitequark: pwning developer machines is pwning production
<q3k>
whitequark: in most cases
<whitequark>
well probably not at facebook
<whitequark>
but yes
<q3k>
whitequark: unless oyu got audit logging, but if you run js on production, you ain't got no audit logging
<whitequark>
would definitely do that at the webdev shop where i worked
<pie__>
didnt something come up here the other day about an attempt to pwn dev machines with a lib
<q3k>
yes, that was an npm package
<pie__>
or rather, someone got pwned and tried to propagate via a malicious lib update
<q3k>
baby's first pastebin | bash malware
<q3k>
stealing npm credentials apparently (payload got taken down before I could analyze it)
<pie__>
(i still dont understand how that got caught so fast, i guess they got lucky that it was shittily coded malware and got some error, but even then, soemone recognized that it was malicious)
<q3k>
tbh pwning npm to pwn more npm credentials is genius
<pie__>
alternatively, it didnt get caught fast and is out there in several more libs?
<whitequark>
to be honest, i'm quite impressed with how fast wasm-compiled solvespace works
<pie__>
q3k, its not clear to me whether this was a "worm" so to speak, i.e. automatically tried to propagate to new libs
<whitequark>
with the exception of some animation hangups that I think are the fault of the way I use emscripten's event loop, it renders around the same fps as my desktop
<q3k>
probably not
<q3k>
pie__: but someone should make one, that'd be super interesting
<q3k>
whitequark: yeah, i guess js engine developers are the unsung heroes of our generation
<whitequark>
wasm bypasses js engine though
<whitequark>
well
<q3k>
whitequark: applying bleeding-edge jit techniques for running all of this swamp
<whitequark>
the wasm<>js interface still matters
<pie__>
you should try to see if anyone managed to save the payload :p
pie__ has quit [Remote host closed the connection]
<awygle>
V8 and spidermonkey are amazing
<whitequark>
that said, the asm.js version is nearly as fast
<whitequark>
so you aren't wrong
pie__ has joined ##openfpga
<bubble_buster>
what does read_verilog -sv do? says it's parsing systemverilog but doesn't seem to have full support
<whitequark>
it "sort of" parses systemverilog
<q3k>
very basic support for sv
<whitequark>
which is to say, it accepts and ignores sv constructs
<whitequark>
like it desugars logic into wire iirc
<awygle>
yup
<bubble_buster>
I see
<q3k>
also always_ff and always_comb and whatnot
<q3k>
but none of the fun stuff
<q3k>
(fun to use, not fun to implement)
<awygle>
if you want the fun stuff you need verific
<pie__>
ugh my internet
<awygle>
which is $$$
<awygle>
iiuc
<pie__>
coq to verilog compiler when
<awygle>
the power is in your hands pie__
<pie__>
well i suppose coq to haskell is a thing so maybe you can do coq to clash to varilog haha
<q3k>
yeah, either bring your own verific license and build yosys yourself, or get a commercial license from symbioticeda and that comes with yosys/verific
* pie__
dies
<pie__>
oh verific is some actual software thing?
<bubble_buster>
is there any way to do sv to ... blif/ilang/liberty that yosys can read?
<pie__>
ah i only skimmed scroll and assumed its some kind of verification thing
<whitequark>
i actually wanted to do coq to verilog
<whitequark>
but coq is like, hard
<q3k>
bubble_buster: verific does that :) not aware of any free/open solutions though
<whitequark>
using smt is cheating
<bubble_buster>
hmm. maybe I can convince university to get a license...
<q3k>
pie__: verific is a library for parsing/elaborating (system)verilog and chdl
<q3k>
pie__: and some more things
<whitequark>
pie__: coq to clash would be as hard as coq to verilog
<q3k>
bubble_buster: there's a chance your university already has a verific license
<q3k>
s,chdl,vhdl,
<q3k>
tl;dr F/LOSS support for SV is non-existant, as far as I remember
<q3k>
which is a bummer
<bubble_buster>
dang. was hoping I could tell students they could use riscv-formal with not much extra effort
<pie__>
whitequark, im not even sure that coq the language it hard (though from what i hear its the best mess we've got, which is a relatively good one), but theres of course plenty of math involved yeah..
<bubble_buster>
don't think they'll want to use verilog as seniors after using systemverilog in most previous classes
* pie__
mumbles something about agda too, but which doesnt seem to be as "practical"
<q3k>
bubble_buster: you can convince some of your students to implement a full systemverilog frontend in yosys :)
<bubble_buster>
That would probably be easier than just using verilog :D
<pie_>
" A natural number is not equinumerous to a proper subset of itself"
<pie_>
see thats not something youd necessarily think of as the thing to try to prove offhand
<pie_>
also > php
<cr1901_modern>
What's "⊢" again?
<pie_>
not sure but you can basically read it as "it can be proved that"
<sorear>
Called a Turnstile
<sorear>
And yes
<pie_>
you can have stuff on the left of it and then it means something like, it can be proved from the stuff on the left that ...
<pie_>
when theres nothing on the left it means you can prove it without additional assumptions
<pie_>
i.e. the stuff on the left
<sorear>
Although Metamath is a Hilbert system and the left side is always empty, it’s kept for … reasons
<pie_>
still havent worked through chiswell & hodges...
<cr1901_modern>
what does the nesting level represent (number to the left of the turnstile)?
<pie_>
but its on my desk...
<pie_>
cr1901_modern, proof starts from the bottom
<pie_>
(sort of)
<cr1901_modern>
(Also, I assume "→" is morally equivalent to boolean implies?)
<pie_>
with the qualification that sorear said this is a hilbert system, which i dont really know anything about
<sorear>
It’s exactly Boolean implies
<sorear>
Tree/DAG structured. Each step is a consequence of previous steps, the last one must match the theorem
<pie_>
ok nevermind, ^ :p
<pie_>
if its like anything like making deduction trees in propositional logic (i think hilbert system means you just write the deduction different), in practice when making a deduction tree it means you can change the left of the arrow into an assumption, and the right becomes the statement to prove
pie_ has quit [Remote host closed the connection]
pie_ has joined ##openfpga
<cr1901_modern>
I'll ask more about it later. It looks fascinating, and I can actually follow most of it (it looks like the stuff you'd see when playing w/ z3)
<sorear>
In practice Hilbert vs Gentzen mostly means that we use the left side of a regular arrow for assumptions instead of a the left side of the turnstile