usi-verification-and-security / opensmt

The opensmt solver
Other
78 stars 18 forks source link

664 explicitly divide debug and release builds #670

Closed Tomaqa closed 9 months ago

Tomaqa commented 9 months ago

Root Makefile that serves only for initial builds.

make (or make default or make release) builds build and make debug builds build-test. make all builds both. Once the build directory is created, the rule is "up-to-date" and not run anymore. This is not a mistake but my intention.

The build directories can also be removed using make clean (or make clean-release) and make clean-debug (or make clean-all). Then it is possible to run e.g. make again.

The target build directories can be modified via cmdline, for example: make RELEASE_BUILD_DIR=build-release. But then the option should also be used for make clean otherwise it will try to remove the default build directory (it won't fail but won't do anything).

More importantly, CMake options may be modified using CMAKE_FLAGS option, for example: make CMAKE_FLAGS=-DENABLE_LINE_EDITING:BOOL=ON make debug CMAKE_FLAGS='-DENABLE_LINE_EDITING:BOOL=ON -DUSE_READLINE:BOOL=ON'

The Makefile is not documented yet, README is not updated.

Resolves #664.

I think that the install rules should be handled too, but here I am not sure how to handle the target install directory for the library (include is the same for both) - should there also be a separate directory for each build type (e.g. /usr/local/lib/release/libopensmt.a and /usr/local/lib/debug/libopensmt.a, or /usr/local/lib/libopensmt.a and /usr/local/lib/debug/libopensmt.a), or should it be just one and always overwrite the previous file? In order to change the build type. I think that on the system level, at least on Linux distros, only one type at a time is usually supported.

Tomaqa commented 9 months ago

I am wondering if this is connected to issue #664 automatically or if it is necessary to do so manually ..?

blishko commented 9 months ago

I am wondering if this is connected to issue #664 automatically or if it is necessary to do so manually ..?

If you add "Resolves #664" to the description, the issue will be automatically closed when the PR is accepted. (You can also use different phrases).

blishko commented 9 months ago

make (or make default or make release) builds build and make debug builds build-test.

This should say that make debug builds build-debug.

Tomaqa commented 9 months ago

Since this only works if the directory does not exist, if I want to rebuild the project after some change, I still have to do it explicitly with cmake --build or in the build directory invoking the build system such as make or ninja, right? So it is only a shortcut when I want to build the project for the first time?

Yes. It can run either always or only once, but nothing in between - unless all source code prerequisites were supplied, which would duplicate the purpose of makefiles in build*. Nonetheless, you can always run make * with -B which skips all prerequisite checks and runs all corresponding rules. This can be used for a "rebuild". ... However, I noticed now that doing so also results in recompiling all related sources, contrary to what e.g. cmake --build does. This is not too convenient.

Therefore, I may change it s.t. the Makefile invokes cmake -B * only once (i.e. every time the build directory does not exist yet) but runs cmake --build * every time. Do you agree? Or do you have better idea?

blishko commented 9 months ago

Therefore, I may change it s.t. the Makefile invokes cmake -B only once (i.e. every time the build directory does not exist yet) but runs cmake --build every time. Do you agree? Or do you have better idea?

Yes, I think that would be good.

Tomaqa commented 9 months ago

Yes, I think that would be good.

Done.

Tomaqa commented 9 months ago

Cool.

I still have this pending question. I think it should also be included in this root makefile. What do you think?

I think that the install rules should be handled too, but here I am not sure how to handle the target install directory for the library (include is the same for both) - should there also be a separate directory for each build type (e.g. /usr/local/lib/release/libopensmt.a and /usr/local/lib/debug/libopensmt.a, or /usr/local/lib/libopensmt.a and /usr/local/lib/debug/libopensmt.a), or should it be just one and always overwrite the previous file? In order to change the build type. I think that on the system level, at least on Linux distros, only one type at a time is usually supported.

blishko commented 9 months ago

I think there should only be one target install directory for both. I guess here you have to explicitly specify which configuration you want to install.

Tomaqa commented 9 months ago

I believe it is done. The installation dir can be customized either within make or be overridden within make install via INSTALL_DIR variable in both cases. Plain make install works as well but only if it does not require sudo, otherwise everything is compiled with root privileges which is not neat. I would not even document this option and would just write to use make && make install (or make && sudo make install). Another problem is that it is not possible to combine root and non-root installations (regardless of the build): sudo make install and make install INSTALL_DIR=local_dir fails because the previous call to CMake still produces some root files. In this case, make clean is necessary. This can still be avoided by using two separate build dirs, one for root installations and the other one for local ones, using RELEASE_BUILD_DIR variable (or debug).

Anyway, the basic setups work perfectly fine. For example: make && sudo make install make && make install INSTALL_DIR=local_dir make INSTALL_DIR=local_dir && make install make install INSTALL_DIR=local_dir make INSTALL_DIR=local_dir && make install && make install INSTALL_DIR=install_dir2

The install rules should behave the same as the build rules - they always check if there is anything that needs to be rebuilt.

If this is fine, I will update the README and it should be completed.

Tomaqa commented 9 months ago

.. and if you want to install the debug build, install-debug must be used instead of install (or install-release).

Tomaqa commented 9 months ago

Updated README.

The last thing is that the executable is for some reason placed at build/opensmt and not at build/bin/opensmt - inconsistently with the installation (e.g. /usr/local/bin/opensmt). Also it is weird that build/bin is actually present but it is empty. However, I have no experience with CMake and I do not know how to achieve that. But I suppose it is easy, when one knows what to do.

Tomaqa commented 9 months ago

Maybe connected to the above, there's this weird bin/opensmt.C. I suppose it is some relict and that src/bin/opensmt.cc is currently being used.

blishko commented 9 months ago

The last thing is that the executable is for some reason placed at build/opensmt and not at build/bin/opensmt - inconsistently with the installation (e.g. /usr/local/bin/opensmt). Also it is weird that build/bin is actually present but it is empty.

This was by design. Or at least for me it was more comfortable. But we can move it to bin folder. And yes, there is some old file, I think the cleanup of bin directory in src should be a separate PR.

Tomaqa commented 9 months ago

And yes, there is some old file, I think the cleanup of bin directory in src should be a separate PR.

671

Tomaqa commented 9 months ago

Should be ready to merge. The last three commits could be squashed, but I am just lazy :stuck_out_tongue: