STP_STUB option leads to build failure

[Vekhir]

STP_STUB option leads to build failure

[quark17]

I didn't realize that this hadn't been fixed! There's a PR #278 open for it. From years ago -- apologies for letting that slip through the cracks!

The issue is that the real STP build leaves this in the src/vendor/stp/lib/ directory:

lrwxrwxrwx ... libstp.so -> libstp.so.1
-rwxr-xr-x ... 2 libstp.so.1

while the stub STP build leaves this:

lrwxrwxrwx ... libstp.so -> libstp.so.1
lrwxrwxrwx ... libstp.so.1 -> libstp_stub.so
-rwxr-xr-x ... libstp_stub.so

The build of the bsc executable in src/comp/ is told to look in that directory for libraries, so it can see all the versions:

STP_LIB_FLAGS = -L../vendor/stp/lib -lstp

And I believe that it follows the links and thus knows what the ultimate name of the library is, and encodes that in the executable. For example, BSC built with the real STP has the following output from ldd bsc:

libstp.so.1 => ...

while BSC built with the stub STP has this ldd bsc output:

libstp_stub.so => ...

So when BSC is run, it needs to find that exact file name in the LD search patch. That would be fine, if we installed all of the file from src/vendor/stp/lib/ into inst/lib/SAT/. But we don't; we only install the file libstp.so.1 as indicated in src/vendor/stp/Makefile:

ifeq ($(OSTYPE), Darwin)
SNAME=libstp.dylib
else
SNAME=libstp.so.1
endif

install:
        ...
        install -m 644 lib/$(SNAME) $(PREFIX)/lib/SAT

This works for BSC built with real STP, but doesn't work for BSC built with the sub (which is expecting to find libstp_stub.so.

The PR #278 attempts to make the STP stub situation work by installing multiple files (the variable SNAME becomes a list of names to install). Do we need to install them all, though? An alternative would be to still install only one name, and just have that name be libstp_stub.so in the stub case. Or, we change the stub build to create libstp.so.1 as the library name, so that the built bsc executable is looking for the same library name in either case. I can see some benefit to having the name indicate that it's a stub, though, so I'm in favor of a different name.

Any preference?

I'm in favor of installing one name, maybe like this:

ifeq ($(STP_STUB),)
SRC = src
else
SRC = src_stub
endif

ifeq ($(OSTYPE), Darwin)

ifeq ($(STP_STUB),)
SNAME = libstp.dylib
else
SNAME = libstp_stub.dylib
endif

else

ifeq ($(STP_STUB),)
SNAME = libstp.so.1
else
SNAME = libstp_stub.so
endif

endif

Or we could fix up the stub Makefile to buld libstp_stub.so.1 and clean up the name construction like this:

ifeq ($(STP_STUB),)
SRC = src
LIBNAME = stp
else
SRC = src_stub
LIBNAME = stp_stub
endif

ifeq ($(OSTYPE), Darwin)
SNAME = lib$(LIBNAME).dylib
else
SNAME = lib$(LIBNAME).so.1
endif

FYI, I notice that trying to build STP_STUB=1 on macOS fails even earlier, because there is no file libstp.dylib (or even libstp_stub.dylib), because the build of the stub specifies .so in the file name. We can change that to .dylib or not; whatever we do should be consistent between the makefiles.

[Vekhir]

I've been working to overhaul the STP_STUB behavior, so I've fixed it there in section "disable STP at runtime".
Essentially, the SNAME is exported to the different Makefiles below to ensure consistency in naming and a single place where the name can change. It's quite similar to the first suggestion.

The fix could be backported to work with the old STP_STUB, but with the new API, we could use this opportunity to remove STP_STUB since it was already broken for years (instead of fixing it and annoying people when removing it later).

[quark17]

We're trying to get a 2023.07 release out. The overhaul needs some discussion, so I don't want to hold up a release for it. I'd just like to get the code in a stable form, to tag a release. The stub flag behaviors have been this way for a while, so it's not a problem to leave it, except that I did add mention of the STP_STUB and YICES_STUB flags to the build instructions. It feels wrong to document it if it's broken -- either we should remove that mention from the docs, or we should quickly fix it up. Unless I'm overreacting and it's fine to document it and leave the behavior as it is?

My thought was just to get STP_STUB=1 to successfully build, by changing the stub object file to have the same name (and maybe install it with a link, so that it's clear to people looking at the installed files that it's a stub, while still being available for loading as the generic name); and to leave the Yices behavior as is, because anyone building with YICES_STUB=1 is already encountering the need to explicitly add -sat-stp when calling BSC. That should be a simple fix and then we can make a release.

On your overhaul, I have some thoughts, but maybe I should wait until I've looked at it more. But off the top of head, I wonder if a build with the system library should just not install any object file and use what's in the system. (I guess that depends on whether such a build wants to require the users to also have the library installed.) Also, my sense has been that an installation can change -- like, if it started with a yices stub, but then someone wanted to add yices, they could change what's in the lib/SAT/ directory (either put a real library in that directory or remove the stub and let the one from the system be found) -- and if that's the perspective we want to support, then the bsc binary should always be looking for the generic name (which can be a link to different implementations) and not looking for an implementation-specific name depending on how the installation was built (like libstp_stub.so or libstp_system.so etc). Also, there have been a lot of proposals of how to replace the current STP/Yices integration with other ways of doing things (see open issues/discussions mentioning STP); if we're putting effort into an overhaul, would it be better to put the effort into one of those bigger overhauls? (At the very least, we might consider using a newer STP. The snapshot we have doesn't have a version function, so we can't even warn the user that the library that's found doesn't match, and I see that the STP in github has a function for getting the version tag.)

[Vekhir]

We're trying to get a 2023.07 release out. The overhaul needs some discussion, so I don't want to hold up a release for it. I'd just like to get the code in a stable form, to tag a release. The stub flag behaviors have been this way for a while, so it's not a problem to leave it, except that I did add mention of the STP_STUB and YICES_STUB flags to the build instructions.

In that case I'd say to postpone this fix until after the release. The feature is so obviously broken that everyone can tell not to use it (or patch it, in which case they are on their own). If this was a subtle bug somewhere, that'd be different.

[...] It feels wrong to document [the STP_STUB and YICES_STUB flags] if it's broken -- either we should remove that mention from the docs, or we should quickly fix it up. Unless I'm overreacting and it's fine to document it and leave the behavior as it is?

Of course, documenting it without testing wasn't a great decision, but the feature is intended to exist, so the documentation isn't wrong per se.
Maybe put a "Known issues" section in the release notes where it says that using the flags (both STP_STUB and YICES_STUB) leads to build failures?

My thought was just to get STP_STUB=1 to successfully build [...]

Any my thought was to precisely not do that if we intend to deprecate it shortly afterwards. If it's absolutely necessary, then getting it to build isn't actually all that difficult (like the NixOS guys have been doing) - and then they know that it might not work with the next release, when the refactor came in.

My thought was just to get STP_STUB=1 to successfully build, by changing the stub object file to have the same name (and maybe install it with a link, so that it's clear to people looking at the installed files that it's a stub, while still being available for loading as the generic name); and to leave the Yices behavior as is, because anyone building with YICES_STUB=1 is already encountering the need to explicitly add -sat-stp when calling BSC. That should be a simple fix and then we can make a release.

If I build it explicitly with the stub, then I'd want STP to be disabled. So not sure why it needs to be available for loading as the generic name. It doesn't need to change. If I later change my mind, then I either have to rebuild BSC (because a build option has changed) or rename my library *_stub if I'm too lazy for that.
Of course we can add an option STP_USE_LIB=disable-at-buildtime-but-maybe-I-change-my-mind-at-runtime which does the desired behavior. The refactored code allows for that.

leave the Yices behavior as is, because anyone building with YICES_STUB=1 is already encountering the need to explicitly add -sat-stp when calling BSC.

On Yices, I don't want to change any behavior, only the flag is supposed to be mirrored in the refactor. If that note comes from the misunderstanding in #599, then we are on the same side.

Thoughts on overhaul/refactor

On your overhaul, I have some thoughts, but maybe I should wait until I've looked at it more. [... Lots of thoughts cut for brevity ...]

Yeah, that's an entirely different discussion, I've opened the draft PR #600 so we can discuss that there.
In short - to not pollute this thread, your thoughts are much appreciated - the big overhaul has two limiting factors on my side:

1. Me wanting to avoid feature creep that leads to lots of changes which in turn delay actually merging all of it, and
2. Me simply not being able to implement the other suggestions. Doesn't mean I can't learn it, but at the moment I'm not particularly interested in that. Also means more delay.

So I settled for a refactor - "overhaul" probably set the wrong expectations - of the Makefiles in order to get a quick and immediate improvement. This discussion should be continued in the draft PR though.