tgamblin

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: ['%pgi@18.5']
        projections:
          all: '{name}/{version}-{compiler.name}'
        link_type: symlink

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}"

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

    view:
      default:
        root: ~/myprefix

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
    ...
    cmake@3.27.9             ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/cmake-3.27.9-x6g5fl54kgt4nqmgnajrtfycivokap2p
    cmake@3.27.9             ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/cmake-3.27.9-x4bznyafesvpdbplqhmnwwvy2zj5fdzs
    coreutils@9.3            ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/coreutils-9.3-vlwyg7d3ysxfoom3erl6ai4yy7fuf2jn
    curl@8.4.0               ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/curl-8.4.0-zjz6twa32vxnevika34kkrxjwo27z6vj
    curl@8.6.0               ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/curl-8.6.0-da5tk7aqaqp6zdligjmahzwohzut65qc
    diffutils@3.9            ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/diffutils-3.9-lau4vo7zlsktmbhyn3pf3x72nxhihsaq
    double-conversion@3.3.0  ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/double-conversion-3.3.0-zihvj7vzedapjprk76awr7qied3k45n6
    emacs@29.2               ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/emacs-29.2-x5v4wdhp4vfsuxquadackqckdvxrppwi
    expat@2.5.0              ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/expat-2.5.0-hmdysf6hcrzuhcxu7fkecpvskzxecgps
    findutils@4.9.0          ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/findutils-4.9.0-atynmdjhdjpb2ipurlk7cxtdep77m7mu
    fish@3.6.1               ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/fish-3.6.1-sg3ws3rmbfgdfyhvjnhd5agepguj4yf2
    flex@2.6.3               ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/flex-2.6.3-quw6ammnjxfutqtqcifvjfsp5nyqpeab
    freetype@2.11.1          ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/freetype-2.11.1-ue2ofutkkawtzvcl47pqts4lasm5lgha
    gawk@5.2.2               ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/gawk-5.2.2-jld7vb24rls64nbzkyxcp4alluyedfzv
    gdbm@1.23                ~/spack/opt/spack/darwin-sonoma-m1/apple-clang-15.0.0/gdbm-1.23-amtpuskagocirjhffgqrjas3bfbnzixi
    ...

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

[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 config blame`. There are different YAML configs, they can be merged and override each other 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 specialized defaults for 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: apple-libunwind@35.3
    spack/defaults/darwin/packages.yaml:28                  prefix: /usr

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 from 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 to other problems in order to show NP-completeness.

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

Love this article and the push to build awareness of what modern SAT solvers can do.

It's worth mentioning that there are higher level abstractions that are far more accessible than SAT. If I were teaching a course on this, I would start with either Answer Set Programming (ASP) or Satisfiability Modulo Theories (SMT). The most widely used solvers for those are clingo [0] and Z3 [1]:

With ASP, you write in a much clearer Prolog-like syntax that does not require nearly as much encoding effort as your typical SAT problem. Z3 is similar -- you can code up problems in a simple Python API, or write them in the smtlib language.

Both of these make it easy to add various types of optimization, constraints, etc. to your problem, and they're much better as modeling languages than straight SAT. Underneath, they have solvers that leverage all the modern CDCL tricks.

We wrote up a paper [2] on how to formulate a modern dependency solver in ASP; it's helped tremendously for adding new types of features like options, variants, and complex compiler/arch dependencies to Spack [3]. You could not get good solutions to some of these problems without a capable and expressive solver.

[0] https://github.com/potassco/clingo

[1] https://github.com/Z3Prover/z3

[2] https://arxiv.org/abs/2210.08404, https://dl.acm.org/doi/abs/10.5555/3571885.3571931

[3] https://github.com/spack/spack

I work at LLNL so I work with people who make cool simulations all the time. The coolest ones I’ve seen lately were the ones that helped with last year’s big fusion ignition shot at NIF.

There is a (very) recent article summarizing how simulations contributed to ignition here: https://www.llnl.gov/news/computing-codes-simulations-helped.... Just reading about how many different simulation teams were involved and how many different types of physics had to be modeled to get that shot to work is awe-inspiring, at least for me. Optimizing target thickness, modeling plasma in the target, laser coupling at the entrance hole, etc. - there are a ridiculous number of things that had to be modeled, together, at very different scales.

The prior article describing how simulation contributed to the pre-ignition, 1.3 MJ shot goes into some more detail and has some cool visualizations: https://lasers.llnl.gov/news/models-and-simulations-help-map.... The one showing the target fill tube perturbing the implosion in 3D stands out to me - it shows the types of tiny things that can cause a fusion shot to go wrong.

Spack packages are parameterized, so there is one `package.py` file per package, not several, and you can have many versions and options declared. See, e.g., `zstd`: https://github.com/spack/spack/blob/develop/var/spack/repos/...

This was a conscious decision we made to allow many versions to be built without requiring split implementations and without checking out different commits -- that saves some work already. It also forces the repo maintainers to consider the other use cases, which tends (IMO) to make the recipes more portable.

But the real question is not just work saving but correctness. You cannot always just swap in libA@2.0 as in your example. For:

    packageX ^libA@2.0 

    1. packageX and libA use the same MPI implementation (e.g., openmpi, mpich, mvapich)
    2. the MPI implementation chosen satisfies the provider requirement
    3. any version/option constraints that packageX has on MPI are satisfied along with those of libA.

This isn't just an overlay; it's a constraint solve. The choice of libA@2.0 can have effects on other nodes in the graph, and different choices may need to be made elsewhere; maybe even things like disabling options or choosing different dependencies.

Maybe I should clarify:

it basically boils down to removing that directory + the environment module file that EasyBuild generated for it

Another important thing is knowing what depends on that package (so you don't remove something else's dependency). This is something that EB doesn't track after installation time.

EasyBuild can install "binary packages"

What I meant here is that EB has no binary packaging system of its own. It has no binary package format, no signing, no way to take an installation and bundle it up into a file that can be installed (potentially in a different location) on another system. Spack, Nix, and Guix all have systems for creating and (re)installing binary substitutes for source builds (we call them build caches). EB can install someone else's binary package/distribution (we can too FWIW), but it can't create its own.

But maybe you're referring to installing software in a shared filesystem (NFS, usually something like /apps).

Yes -- specifically that, with environment modules. Spack installations similarly all go in their own directories, but you can compose them in many different ways with environments and views. e.g., you can:

    - Create a symlink tree of many packages together in a common prefix (a view)
    - "project" package installations into different directory layouts with symlinks, hardlinks, or relocated copies

And you don't have to load packages one by one with modules. You can avoid modules entirely with `spack load` or use `spack env activate` to put everything in an env into your `PATH` (and other env vars).

So how would I know whether the prebuilt binaries were built in a longer path than I install to?

All the public ones are built with very long padding; if you make your own you're currently on your own.

Is there at least a way to block source builds if the app is not in the binary cache to avoid any surprises (basically have manual override/confirmation instead of automatic fallbacks to source builds)?

Yep:

    spack install --cache-only ...

do prebuilt binaries rerouted to be installed in a predefined path they were built in or is it also flexible?

Prebuilt binaries don't have to go in a fixed prefix -- we'll relocate RPATHs, shebangs, strings in text files, and (as long as you build in a longer path than you install to -- see `padded_length` at https://spack.readthedocs.io/en/latest/config_yaml.html) strings in binaries.

There is not currently a way to see before you install if an install will be from binary or from source, but that is something we are working on.

Yep, it works with Lmod (https://lmod.readthedocs.io) and environment modules (https://modules.sourceforge.net). See the tutorial on setting up modules for what the integration looks like:

* https://spack-tutorial.readthedocs.io/en/latest/tutorial_mod...

AFAIK environment modules are implemented in TCL, not perl. The original was in C with an embedded TCL interpreter, but when CEA revived the project w/version 4 in 2017, it was all in TCL.

HPC isn't exactly special, and neither to some extent is Spack. Spack's gotten some attention in talks at, e.g., CppCon.

The big differentiator is really the degree to which people want to tune and customize their builds in HPC vs. other communities, and the diversity of hardware that needs to be supported. Things that stand out to me:

  - different applications' needs to customize the builds of their dependencies
    - e.g., one app might need HDF5 with MPI support, another might want it 
      built without. Those are two different, incompatible HDF5 builds.
  - need for specific microarchitecture builds to take advantage of vectorization
  - need for GPU support (for NVIDIA, AMD, *and* Intel GPUs)
  - need to use sometimes vendor-specific tuned system libraries like MPI, cray-libsci, mol
  - need for specific *versions* of dependencies (solvers, mesh libs, etc.) for
    numerical reproducibility
  - need to integrate across languages, e.g. C, C++, Fortran, Python, Lua, perl, R,
    and dare I even say Yorick.

So I'd say Spack is not so much a special package manager as a much more general one. You can use it for combinatorial deployments at HPC centers, dev workflows for people dealing with multi-physics and other complex codes, and as sort of a distributed poly repo with lock files.

The intent was never to be specific to HPC, and I would love to see broader adoption outside this community.