bluehs: run scripts against the compiled library; make install-bluehs - #1119
Open
matx-jeffnewbern wants to merge 18 commits into
Open
matx-jeffnewbern wants to merge 18 commits into
matx-jeffnewbern wants to merge 18 commits into
Conversation
This breaks the Makefile, and doesn't replace everything it did, but it's sufficient to build binaries and run tests on Linux.
The bin wrapper scripts used to set BLUESPECDIR; with the solvers statically linked, that was their last remaining job. Instead, let bsc, bluetcl, showrules and vcdcheck fall back to <exedir>/../lib (recognized by its Libraries subdirectory) when BLUESPECDIR is unset, and write the result back to the environment for the subprocesses that read it (simulator build scripts, generated Bluesim executables, and the Tcl side of bluetcl). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JW5cpDCo9whk4PCg9kn6ea
Every executable target runs `ghc --make` into the same -odir, so two of them
running at once race on the objects of the modules they share: one renames its
temporary over the path the other is still writing. Under `make -j10
install-extra` this appeared as
renameFile:renamePath:rename '.../build/comp/VCD.o.tmp' to
'.../build/comp/VCD.o': does not exist
make: *** [fstcheck] Error 1
with two targets compiling VCD at the same time.
GNU Make 3.81 is still in use, and it has no per-target .NOTPARALLEL, so the
aggregate targets build through a sub-make invoked with -j1. That holds
whatever -j the caller passed. The cost is small because the objects are
shared: measured over a rebuild forced by touching VCD.hs, the whole serial
install-extra took seven seconds, since after the first target the rest
compile only their own main and link. GHCJOBS still parallelises within each
compile, and naming one executable directly still builds only that one.
The cabal build moves every program's entry module into src/comp/app, so that they are executables separate from the library, and replaces bluetcl_Main.hsc with a pre-generated bluetcl_Main.hs plus a C shim. The Makefile did not follow, so it found no main at all: `ghc --make bsc` reports `target 'bsc' is not a module name or a source file`. Each moved target now names its own source file through MAINSRC, because the file name does not always match the executable. Targets whose main is still beside the library modules keep the default and are untouched. app joins the module search path, so BlueTcl resolves as imported by bluetcl_Main. bluetcl builds in one step from that entry module and shim, which is how the cabal executable is built too, leaving one bluetcl entry point to maintain rather than two. It gains the shared RTS options in the process, matching what the cabal stanza gives the other executables. -o $@ moves into the shared flags, because a target named by its app/ path would otherwise link next to its source. The previous default output name was already the target name, so nothing else changes, including the profiling and debug builds.
Every bsc executable was installed as a copy of wrapper.sh in bin/. The script set BLUESPECDIR from its own location, put $BLUESPECDIR/SAT on LD_LIBRARY_PATH and DYLD_LIBRARY_PATH, and exec'd the real binary out of bin/core/. getBluespecDir already derives the directory from the executable's own path, so the library path was the only job left, and an rpath does that without a script in the way. On macOS an rpath is not enough on its own. Mach-O consults LC_RPATH only for a dependency recorded as @rpath/..., and the vendored solvers record bare names, which dyld resolves through its default search and nothing else. Each solver therefore records itself @rpath-relative, through the knob its own build already provides: -install_name for STP, and the libyices_install_name that yices' configure accepts and that this tree was already overriding to strip yices' absolute default. ELF needs none of it, because a soname is what the linker writes into whatever links a library and the installed files carry those names. The rpath is @loader_path/../lib/SAT, or $ORIGIN/../lib/SAT on ELF, and it is the only entry. It resolves bin/<name> to lib/SAT, where src/vendor installs the solvers before src/comp installs anything. Being relative is what keeps the top-level Makefile's promise that an installation can be moved anywhere as long as its contents keep their relative positions, and it leaves no build-tree path for a distribution to strip out of a shipped binary. Only bsc and bluetcl link a solver, so only they carry it. The executables now install directly as bin/<name> and bin/core is gone. Nothing referred to that path. The System 81 text loses its mention of BLUESPEC_LD_LIBRARY_PATH, which the wrapper was the only reader of. LD_LIBRARY_PATH still overrides an rpath, so the rest of that advice stands.
The version bounds are caret bounds set to the versions GHC 9.6.7 bundles, and a caret bound on a compiler-bundled package admits exactly one GHC series. base ^>=4.18.3.0 excludes 9.10's 4.20, and the same holds for bytestring, containers, deepseq, filepath, text, unix and process. The make build has no bounds at all and works from 9.6 through 9.14, so the cabal file is the only thing tying the package to one compiler. The thirteen bundled packages get plain lower bounds at 9.6.7's versions with no upper bound, in every stanza: the library, custom-setup, the executables and the test-suites. The Hackage dependencies -- old-locale, old-time, regex-compat, split, strict-concurrency, syb -- keep their caret bounds, which describe ranges rather than a compiler. process needed its floor moved down rather than up. ^>=1.6.28.0 excludes the version both compilers bundle (1.6.19.0 on 9.6.7, 1.6.26.1 on 9.10.3), so cabal built process from Hackage on every machine, and Hackage's 1.6.30.0 does not compile against the filepath GHC 9.10 ships. That floor was carrying something: SetupHooks.hs used callCreateProcess, which System.Process first exported in process-1.6.28. It is four lines over createProcess and waitForProcess, so it is spelled out locally instead, and the setup hooks build against whatever process the compiler brings. Verified by a full cabal build, library and every executable, under GHC 9.6.7 and under 9.10.3. 9.12 and 9.14 are untested: the bounds no longer exclude them, but nothing has been compiled against them.
The solvers arrived as static archives carried in extra-bundled-libraries, which serves the executables and defeats everything that loads the library rather than linking it. Cabal keeps bundled libraries off the bundling component's own link line, so the dynamic object that ghci and runghc load had 186 unresolved solver symbols and failed at dlopen. Declaring the same archives in extra-libraries instead puts them on that link line, but then GHC's runtime linker tries to load them and cannot: a static archive on aarch64-darwin hits an unsupported relocation type and aborts. So the solvers are shared libraries again, as they were before this package existed. The configure hook builds the vendored trees and injects their directories into every component through extraLibs and extraLibDirs, the way the Tcl hook injects what platform.sh reports, because an absolute path in a build tree cannot be written in the .cabal file. It also names an rpath, which is the whole of what either platform needs to resolve the solvers now that they record themselves as @rpath/..., and the vendored directories are the right entry because these artifacts run where they are built. Naming it on the library alone is enough: cabal derives none of its own for these components, and an executable that links the library inherits the library's ldOptions. Injecting it per component instead passes each -rpath twice, which the linker warns about on every link. util/bluehs/setup.sh loses the second build and the generated cabal.project.local it used to write, which existed only to link the archives into the dynamic object after the fact. The launcher loses -Wno-missed-extra-shared-lib: GHC emitted that warning because the registration named libraries with no shared flavour to find, and now there is one. Verified under GHC 9.6.7 on macOS and GHC 9.10.3 on Linux: the library and all eight executables record both solvers and run, a util/bluehs script and a ghci session load the library and call into both solvers, and the warning is gone.
The HLS and GHCi checks run from src/comp and name bsc.hs, which now lives in src/comp/app. HLS falls back to reading the argument as a directory and fails with "Couldn't find any .hs/.lhs files inside directory: bsc.hs", on every platform and GHC. The GHCi check names the same missing file behind it. gen_hie.py builds the HLS cradle from a list of directories that might hold Haskell sources, and .ghci sets the GHCi include path from its own list. Neither had app, so the entry modules were in no include path and in no source list. Both gain it, and the two checks name app/bsc.hs. Verified on macOS under GHC 9.10.3: gen_hie.py writes a cradle listing all nine app sources and -i./app; `haskell-language-server-9.10.3 app/bsc.hs` completes with 1 file worked, 0 failed; and `:load app/bsc.hs` loads 227 modules, which the workflow's own grep reads as a pass. Co-authored-by: Claude <ai.claude@matx.com>
…rary With the compiler built as a cabal library and the program entry modules under src/comp/app, those programs can also be run by runghc against the compiled library rather than as binaries of their own, and ghci can import the whole compiler. There is no second copy of any program. runghc executes a file's main whatever the module is called, so src/comp/app/dumpbo.hs -- module Main_dumpbo, the same file the dumpbo executable is built from -- is itself the script. The launcher resolves a tool name to that file, and bin/ holds one symlink per tool, dispatching on the name it was invoked as. cabal.project names the repository as the project, asks for -O2 to match the make build, and sets write-ghc-environment-files: always, so a bare runghc or ghci resolves the compiled library from anywhere in the tree. The launcher picks the environment file matching the version of the ghc it will run, so a tree built for one compiler is never handed to another. setup.sh is a single cabal build. It exists for its documentation as much as the command: the library has to be rebuilt whenever bsc is rebuilt at a new commit, because .bo and .ba files embed the build version string and the library refuses a .ba whose stamp differs from its own.
Builds bsc-bluehs-<os>-<arch>-<version>.tar.gz, the companion artifact
to the main bsc tarball: a relocatable tree with a pruned GHC runtime
(no profiling/static ways, docs, or unused tools), a ${pkgroot}-relative
package store holding the bsc library and its dependencies, the SAT
solver shared libraries, the utility scripts, and a bin/bluehs launcher.
Tarball users run Haskell scripts against the compiler library with no
Haskell toolchain installed; host requirements are glibc, libgmp,
libtcl8.6 and a C compiler (GHC probes it when loading libraries, and
CPP scripts preprocess with it).
Both tarballs must come from the same commit: the packaged library
embeds the build version string and rejects .ba files from a different
bsc. Ship them from one release action, versioned in lockstep.
LICENSES/ covers everything redistributed: LICENSE.ghc, the SAT solver
texts, and a generated LICENSE.ghc_pkgs enumerating every shipped
Haskell package with license and copyright (make-ghc-pkg-info.sh over
the exact shipped closure, which also fails the build if a non-BSD
license appears).
The build smoke-tests the assembled tree in a scrubbed environment
before packaging. Validated end-to-end on linux-x86_64/GHC 9.6.7
(106 MB compressed).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The library is built in place rather than installed: installing a local package goes through a source distribution, which lacks the vendored solver sources the hooks build. The in-place library then joins the shipped store as one more package. The tool entry scripts come from src/comp/app; the launcher puts a script's directory on the import path.
`bluehs [-i<dir>]... <tool|script.hs> [args...]` passes each -i to runghc, so a script split across several modules can run. The arguments stay in "$@", so a directory containing spaces survives. The same launcher also runs from an installed distribution: when <dir>/../hs/bsc.env exists beside it, it uses the bundled runghc, that package environment and the scripts directory, and defaults BLUESPECDIR to the lib directory of the bsc installation around it.
`make install-bluehs`, after `make install-src`, runs mk-dist.sh to install the distribution at inst/bluehs instead of writing a separate tarball, so it ships inside the bsc installation it must match. It installs the bluehs launcher rather than generating its own copy. - Every search path and dependency of the packaged shared libraries that names the build machine is rewritten relative to the library, with patchelf on Linux and install_name_tool on macOS (re-signed ad hoc), or dropped; the script fails if one survives. The solvers then load without LD_LIBRARY_PATH. - The generated cabal.project pins an index-state, so the commit fixes the dependency set. - cabal's store directory is found rather than assumed, since newer cabal appends an ABI hash to its name. - The smoke test runs a copy of the installed tree from another directory, with the build tree moved aside, under an empty environment. It calls both solvers and checks that the library's build version matches the installation's bsc.
GHC's loader asks the C compiler (--print-file-name) for every library a package names, and GHC's boot packages name system libraries: libc, libm, libgmp, librt, libdl, libstdc++ and libtinfo. Those already load as dependencies of GHC and of the packages' shared objects, so the names are dropped from the distribution's global package database, as the bsc library's registration already drops Tcl and zlib. A script then runs where no C compiler is on PATH, such as a Bazel sandbox that hides the host's; only scripts that use CPP still need one. The smoke test runs its probe with nothing on PATH but what the launcher and the GHC wrappers use.
The script recovered a package's name by stripping the hash from its installed id, then looked it up with ghc-pkg field <name-version>. On macOS cabal-install drops the vowels from the name when it forms a store id (old-locale becomes ld-lcl-1.0.0.7-1ff3ddac), so walking a cabal store failed with "cannot find package ld-lcl-1.0.0.7" and stopped mk-dist.sh at its LICENSES step. Resolve each command-line name to its id once, look every field up with --ipid, and take the package name from the name field. Output for the release tarball's package list is unchanged.
matx-jeffnewbern
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacks on #1117, which stacks on #1084; the diff includes their commits until they merge.
Adds
bluehs, which runs Haskell scripts against the compiled bsc library, either from a checkout or from an installation.In a checkout built with cabal (
util/bluehs/setup.sh):util/bluehs/bluehs <tool> [args]runs a program fromsrc/comp/appwithrunghcinstead of compiling it.runghcruns a file'smainwhatever its module is called, so the file an executable is built from is also its script, and there is no second copy.util/bluehs/binhas one symlink per tool. The launcher dispatches on the name it was invoked as..hsfile can be given by path. Each-i<dir>before it adds a directory to the import path, for a script split across modules.cabal.projectbuilds at-O2, like the make build, and writes a GHC environment file, sorunghcandghcifind the library from anywhere in the tree. The launcher picks the environment file that matches itsghc.The library has to be rebuilt whenever bsc is rebuilt at a new commit.
.boand.bafiles carry the build version, and the library rejects a.bafrom any other build.make install-bluehs, run aftermake install-src, installs the same capability atinst/bluehs, so scripts can run on a machine with no native Haskell toolchain. Building it needsghc,cabal,python3, and on Linuxpatchelf.install_name_toolon macOS), soinstcan still be moved. The build fails if any path to the build machine remains.index-state.inst/bin/bsc.util/bluehs/mk-dist.shbuilds the installation.make-ghc-pkg-info.shnow looks packages up by installed id, because cabal's store ids on macOS drop the vowels from package names.Besides new files, the PR changes the top-level
GNUmakefile,src/comp/make-ghc-pkg-info.sh, and five.gitignorelines.Testing
-hide-all-packages. The commits since that run change no compiler source.make install-bluehspasses on Debian and on macOS with GHC 9.10.3, including the smoke test's run with no C compiler onPATH. On Debian, a two-module script and a script calling libc and libm through the FFI also run from a copy of the installation with no C compiler onPATH.make-ghc-pkg-info.shprints the same output as before forsrc/comp/Makefile's package list, on both platforms.runghcscript against a real.bo, and aghcisession calling into both solvers.