tgamblin

Spack, at least, is also very much at home outside the HPC environment. Works on macOS and Windows (though Windows packages aren't quite as mature as Linux and macOS). Doesn't require environment modules to use.

Also, latest Spack builds in parallel. You can do that with pkgsrc using external tools like Bob [1], but Spack sets up a GNU jobserver, which LLVM and ninja now support in addition to gmake. So you get very dynamic parallelism. See the FOSDEM talk [2].

[1] https://github.com/jperkin/bob

[2] https://archive.fosdem.org/2026/schedule/event/DHUQAN-spack-...

The more recent Lifschitz book is the easiest to learn from IMO:

- https://www.cs.utexas.edu/~vl/teaching/378/ASP.pdf

It starts with basics of using ASP and gives examples in clingo, not math.

The Potassco book is more comprehensive and will help you understand better what is going on:

- https://potassco.org/book/

Things I don't like include that it's more dense, doesn't use clingo examples (mostly math-style examples so you kind of have to translate them in your head), and while the proofs of how grounding works are interesting, the explanations are kind of short and don't always have the intuition I want.

I still think this is the authoritative reference.

The "how to build your own ASP system" paper is a good breakdown of how to integrate ASP into other projects:

- https://arxiv.org/abs/2008.06692

The Potassco folks are doing amazing work maintaining these tools. I also wish more people knew about them.

EDIT: I forgot to mention that specifically for games stuff like enclose.horse, look at Adam Smith's Applied ASP Course from UCSC:

- https://canvas.ucsc.edu/courses/1338

Forgot to mention that one... we use clingo in Spack for dependency solving and other applications frequently slip my mind.

I do for macOS and Linux :). Windows support is also coming along.

There isn’t anything particularly special about the HPC world other than the need for many different configurations of the same software for many different CPU and GPU architectures. You might want to have several versions of the same application installed at once, with different options or optimizations enabled. Spack enables that. Environments are one way to keep the different software stacks separate (though, like nix, spack uses a store model to keep installs in separate directories, as well).

> Datalog is a declarative logic programming language. While it is syntactically a subset of Prolog, Datalog generally uses a bottom-up rather than top-down evaluation model. This difference yields significantly different behavior and properties from Prolog. It is often used as a query language for deductive databases.

https://en.m.wikipedia.org/wiki/Datalog

Spack doesn't require any particular prefix... it has a deployment model like nix, and the store can go anywhere. Binary caches are relocatable.

It's disappointing that this response linked by OP was posted at all. And even more disappointing because context gets lost every time it shows up on HN.

The linked email is from an HPE/Cray employee interacting with the upstream gcc team, not from anyone in the U.S. government.

The U.S. Government, via lots of programs, national labs, etc. does pay people (and companies) to work on open source code. This has at various points included LLVM, clang, flang, gcc, and many other projects. We like it when things get upstreamed and we also contribute ourselves to these projects.

Certain companies' willingness to put in the work required to upstream has been an issue at times, but it is improving and it's something that we push on very hard.

> Maybe it's possible to have multiple _views_ of a filesystem, so via one API you "see" a flat namespace with hashed directories, and with another a conventional hierarchical one

Spack supports the notion of arbitrary "views" of the store, which can be defined declaratively [1]. Apparently we need to write more highlight blog posts and submit them here b/c people don't seem to know about this stuff :)

For example, if you want to make a view that included only things that depend on MPI (openmpi, mpich, etc.), but not things built with the PGI compiler, in directories by name, version, and what compiler was used to build, you could write:

    view:
      mpis:
        root: /path/to/view
        select: [^mpi]
        exclude: ['%[email protected]']
        projections:
          all: '{name}/{version}-{compiler.name}'
        link_type: symlink

That will get you symlinks to the prefixes of the packages that match the criteria, with fancy names.

If you wanted a different layout you might do:

    view:
      myview:
        projections:
          zlib: "{name}-{version}"
          ^mpi: "{name}-{version}/{^mpi.name}-{^mpi.version}-{compiler.name}-{compiler.version}"
          all: "{name}-{version}/{compiler.name}-{compiler.version}"

That puts all your zlib installs in a short name-version directory, most things in directories named by the package and version and a subdirectory for what compiler it was built with, and for packages that depend on MPI it also adds the MPI implementation (openmpi, mpich, etc.) and its version to that.

You can choose to map everything into a single prefix too:

    view:
      default:
        root: ~/myprefix

That is useful for what we call a "unified" environment where there is only one version of any particular package -- it basically converts a subset of a store into an FHS layout.

There are options for choosing what types of links to use and what types of dependencies to link in, e.g., you could exclude build dependencies if you didn't want the cmake you built with to be linked in.

[1] https://spack.readthedocs.io/en/latest/environments.html#fil...

FWIW this is what Spack does, and it uses a store layout like nix/guix. here are some chunks of the spack install tree path. All you really need is the hash, but we provide a bit more.

    $ spack find -p
    ...
    [email protected]             ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/cmake-3.27.9-x6g5fl54kgt4nqmgnajrtfycivokap2p
    [email protected]             ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/cmake-3.27.9-x4bznyafesvpdbplqhmnwwvy2zj5fdzs
    [email protected]            ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/coreutils-9.3-vlwyg7d3ysxfoom3erl6ai4yy7fuf2jn
    [email protected]               ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/curl-8.4.0-zjz6twa32vxnevika34kkrxjwo27z6vj
    [email protected]               ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/curl-8.6.0-da5tk7aqaqp6zdligjmahzwohzut65qc
    [email protected]            ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/diffutils-3.9-lau4vo7zlsktmbhyn3pf3x72nxhihsaq
    [email protected]  ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/double-conversion-3.3.0-zihvj7vzedapjprk76awr7qied3k45n6
    [email protected]               ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/emacs-29.2-x5v4wdhp4vfsuxquadackqckdvxrppwi
    [email protected]              ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/expat-2.5.0-hmdysf6hcrzuhcxu7fkecpvskzxecgps
    [email protected]          ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/findutils-4.9.0-atynmdjhdjpb2ipurlk7cxtdep77m7mu
    [email protected]               ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/fish-3.6.1-sg3ws3rmbfgdfyhvjnhd5agepguj4yf2
    [email protected]               ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/flex-2.6.3-quw6ammnjxfutqtqcifvjfsp5nyqpeab
    [email protected]          ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/freetype-2.11.1-ue2ofutkkawtzvcl47pqts4lasm5lgha
    [email protected]               ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/gawk-5.2.2-jld7vb24rls64nbzkyxcp4alluyedfzv
    [email protected]                ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/gdbm-1.23-amtpuskagocirjhffgqrjas3bfbnzixi
    ...

You can also customize the install tree paths[1] with format strings; the default is:

    config:
      install_tree:
        root: $spack/opt/spack
        projections:
          all: "{architecture}/{compiler.name}-{compiler.version}/{name}-{version}-{hash}"

One reason `nix` uses `/nix/HASH` is because it results in shorter paths and avoids issues with long paths. We use sbang[2] to avoid the most common one -- that long shebangs don't work on some OS's (notably, most linux distros).

[1] https://spack.readthedocs.io/en/latest/config_yaml.html#conf...

[2] https://github.com/spack/sbang

There is also `spack develop`, on which people are building hack/build/test loops. You can `spack develop` any package in spack, and easily build with a modified version of something.

See also https://github.com/sandialabs/spack-manager.

This is stolen from @Theophite, sadly now banned: https://images.app.goo.gl/Rv5SK1qqWXZVNSZ56

> I can't count the number of times I've seen people say "md5 is fine for use case xyz" where in some counterintuitive way it wasn't fine.

I can count many more times that people told me that md5 was "broken" for file verification when, in fact, it never has been.

My main gripe with the article is that it portrays the entire legal profession as "backwards" and "deeply negligent" when they're not actually doing anything unsafe -- or even likely to be unsafe. And "tech" apparently knows better. Much of tech, it would seem, has no idea about the use cases and why one might be safe or not. They just know something's "broken" -- so, clearly, we should update immediately or risk... something.

> Just use a safe one, even if you think you "don't need it".

Here's me switching 5,700 or so hashes from md5 to sha256 in 2019: https://github.com/spack/spack/pull/13185

Did I need it? No. Am I "compliant"? Yes.

Really, though, the main tangible benefit was that it saved me having to respond to questions and uninformed criticism from people unnecessarily worried about md5 checksums.

Which part was hand-wavy/unreasonable? Do you think that dedicated MD5 hardware could become billions or even millions of times more efficient within a decade? If so, why?

The article mentions the key detail: MD5 is broken for cryptography (collisions) but not for second preimage attacks.

I was hoping there would be some discussion of just how much more difficult the latter is. It is extremely difficult.

Let’s ignore that no second preimage attack is currently known for MD5. The software the author links to has a FAQ that links to a paper that lays out the second preimage complexity for MD4:

https://who.paris.inria.fr/Gaetan.Leurent/files/MD4_FSE08.pd...

It takes 2^102 hashes to brute force this for MD4, which is weaker than MD5. A bitcoin Antminer K7 will set you back $2,000, and it gets 58 TH/s for sha256, which is slower than MD5 or MD4. Let’s ignore that MD5 is more complex than MD4, and let’s say conservatively that similar hardware might be twice as fast for MD5 (SHA256 is really only 20-30% slower on a cpu). It’ll take 2^102/58e12/2/60/60/24/365, or about 1.4 billion years to do a second preimage attack with current hardware. So you could do that 3 times before the sun dies.

If you want to reduce that to 1.4 years, you could maybe buy a billion K7’s for $2 trillion. And each requires 2.8kW so you’ll need to find 2.8 terawatts somewhere. That’s 34 trillion kWh for 1.4 years. US yearly energy consumption is 4 trillion kWh.

It will be a while, probably decades or more, before there’s a tractable second preimage attack here.

Yes, there are stronger hashes out there than MD5, but for file verification (which is what it’s being used for) it’s fine. Safe, even. The legal folks should probably switch someday, and it’ll probably be convenient to do so since many crypto libraries won’t even let you use MD5 unless you pass a “not for security” argument.

But there’s no crisis. They can take their time.

In Spack we rewrite strings in binaries, strings in text files (including shebangs), and RPATH/RUNPATH values. It's not hard to find store prefixes in binaries -- they have hashes in them so they're easy to identify. It's hard to lengthen them -- things in text files and in ELF fields can be made longer, but to make strings longer you need to find all references to them, which is impractical. So we build with long paths.

Relocating is really only a matter of relocating prefixes.

I am not sure how it would affect a content-addressed nix store, but I'm also not 100% sure why you want a content-addressed nix store. Addressing by the derivation hash (which is also what Spack does) lets you find valid build substitutes... would you index that separately for a content-addressed store?

Is the goal to allow multiple versions of non-reproducible builds in the same store?

Spack dev here. Yep it's mainly used in HPC, but we'd love to see more folks using in other areas.

There is windows support now (in addition to linux and macOS), which I think was a roadblock for many, and we have gotten some very interest from folks outside the HPC community, e.g. Replica.one, who hope to use it for a software-defined OS for embedded devices: https://www.youtube.com/watch?v=sMxNafpDhng (skip to ~12min for some discussion of Spack, Nix, Guix, and portage)

I’ve done exactly this to manage a test user identity separately from my main GitHub identity, for debugging GitHub apps. I didn’t clone separately, though. I added separate remotes to the repo so I could push a branch to either `github` or `github-test`, and those were associated with the separate hosts/identities from my ssh config.

It looks like you can't search "all" anymore. But if you want the same effect you can hack the URL.

Specifically:

&type=all used to work, but isn't an option anymore

&type=story&type=comment seems to do the same thing now (even if it doesn't show up properly in the pulldown menu).

Would be nice if they put "all" back.

FWIW, we do something like this in Spack[1] with `spack blame`. There are different YAML configs, they can be merged based on precedence, but we tell you where all the merged values are coming from. Here's a simplified example -- you can see that some settings are coming from the user's "default" environment, some from Spack's defaults, and some from specific defaults from Darwin:

    > spack -e default config blame packages
    ---                                               packages:
    spack/environments/default/spack.yaml:59            fftw:
    spack/environments/default/spack.yaml:60              require: ~mpi
    spack/etc/spack/defaults/darwin/packages.yaml:17    all:
    spack/defaults/packages.yaml:18                       compiler: [apple-clang, gcc, clang]
    spack/defaults/darwin/packages.yaml:20                providers:
    spack/defaults/darwin/packages.yaml:21                  unwind: [apple-libunwind]
    spack/defaults/packages.yaml:20.                        blas: [openblas, amdblis]
    spack/defaults/packages.yaml:21                         jpeg: [libjpeg-turbo, libjpeg]
    spack/defaults/packages.yaml:22                         lapack: [openblas, amdlibflame]
    spack/defaults/packages.yaml:23.                        mpi: [openmpi, mpich]
    spack/defaults/darwin/packages.yaml:22              apple-libunwind:
    spack/defaults/darwin/packages.yaml:23                buildable: False
    spack/defaults/darwin/packages.yaml:24                externals:
    spack/defaults/darwin/packages.yaml:27                - spec: [email protected]
    spack/defaults/darwin/packages.yaml:28                  prefix: /usr

The filenames are shown in color in the UI; you can see what it really looks like here: https://imgur.com/uqeiBb5

For the curious, there is more on scopes and merging [2]. This isn't exactly easy to do -- we use ruamel.yaml [3], but had to add our own finer-grained source attribution to get this level of detail. There are also tricky things to deal with to maintain provenance on plain old Python dict/str/list/etc. objects [4,5].

[1] https://github/spack/spack

[2] https://spack.readthedocs.io/en/latest/configuration.html

[3] https://yaml.readthedocs.io/en/latest/

[4] https://github.com/spack/spack/blob/95ca9de/lib/spack/spack/...

[5] https://github.com/spack/spack/blob/95ca9de/lib/spack/spack/...

"It failed after 25 dives" is not a 4% failure rate if the failure was caused by deterioration over time (as it likely was here). It's a 100% failure rate over the full life of any given Titan sub. They'll all implode, given enough trips.

Moreover, both 1% and 4% are horrible failure rates for anything meant to carry passengers. Example: the risk of dying in a commercial plane crash is 1 in 11 million [1]. The risk of dying while skydiving is less than 1 in 300,000 per jump.

This guy was taking extremely unreasonable risks.

[1] https://www.pbs.org/wgbh/nova/planecrash/risky.html

[2] https://dzoneskydiving.com/articles/how-many-people-die-skyd...

Dart as in the language? Dart uses a SAT solver: https://github.com/dart-lang/pub/blob/master/doc/solver.md

Yep, from SAT. Edited. Guess I typed that too fast :)

I read Potassco's Answer Set Solving in Practice book [0] but it's pretty dense. I suspect it would be easier to digest if you read it while also following their course materials, which are all online [1].

These days I recommend people start with the Lifschitz book [2] and read through the Potassco book [0]. Lifschitz's book is a much gentler introduction to ASP and logic programming in general and its examples are in ASP code (not math). It's also more geared towards the programming side than the solving side, which is probably better for most people until they really want to understand what clingo/gringo/clasp are doing and what their limitations are.

There are other more applied courses, like Adam Smith's Applied ASP course at UCSC [3]. The problems in that course look like a lot of fun.

[0] https://potassco.org/book/

[1] https://teaching.potassco.org

[2] https://www.cs.utexas.edu/users/vl/teaching/378/ASP.pdf, https://www.amazon.com/Answer-Set-Programming-Vladimir-Lifsc...

[3] https://canvas.ucsc.edu/courses/1338

I definitely recall doing reductions to SAT in Algorithms courses. I think that is a common part of most curricula.

I don't recall being taught any practical uses of SAT. It was introduced only in the context of Cook's theorem, as the problem you needed to reduce other problems to in order to show NP-completeness.

I think most people now learn SAT in that theoretical context, not as a tool to solve problems.