Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

build: support a system CUDD installation #48

Merged
merged 1 commit into from
Sep 11, 2020
Merged

build: support a system CUDD installation #48

merged 1 commit into from
Sep 11, 2020

Conversation

jengelh
Copy link
Contributor

@jengelh jengelh commented Sep 8, 2020

libbrial/include/polybori/cudd can be made into a symlink to
/usr/include/cudd. With that, two brial-specific files, prefix.h and
prefix_internal.h need to be moved elsewhere, hence the new cuddaux
directory.

Afterwards, one will notice compile errors because PBORI_PREFIX is
undefined; this is because .cc files previously failed to include
prefix.h and relied on some implicit inclusion through another file
(not good), hereby fixed as well.

From there, one can abolish the symlink (again) and use an actual -I
argument to the compiler, editing "#include" lines as needed, and
offer the cudd include directory as a parameter through configure.ac.

@kiwifb
Copy link
Member

kiwifb commented Sep 10, 2020

Sorry for the delayed answer. This is rather cool! More than cool, that has been a wish list item for a long time.

What annoys me a little bit is that the CI doesn't seem to run on your pull request. I would have liked to have that validation before merging.

In any case I have a couple of questions:

  1. does this work with recent versions of CUDD?
  2. Is CUDD stable enough that we won't have to worry too much about changes in the next few years?

Speaking of CI, if we can use external CUDD, it would good to extend the CI to test building against a recent (preferably latest version) of CUDD.

configure.ac Outdated
@@ -95,6 +95,16 @@ else
fi
fi

SYSTEM_CUDD=""
AC_ARG_WITH([cudd],
[AS_HELP_STRING([--with-cudd=includedir], [Utilize a system-installed CUDD library])],
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't really like this part. --with-external-cudd with it being yes or no would be better in my mind. If you need an include directory, then it should be a more specific flag. And then you would expect a matching flag for the library directory.
I would prefer not to take any include directory if possible but test header presence and possibly library presence with AC_CHECK_HEADER and AC_CHECK_LIB.
This may mean that we have to use macro (like SYSTEM_CUDD) to get the right header location.

@kiwifb
Copy link
Member

kiwifb commented Sep 10, 2020

The CI actually did run but failed. This point to a few more details needing fixing at install time I believe. Look at https://travis-ci.org/github/BRiAl/BRiAl/jobs/725307404

libbrial/include/polybori/cudd can be made into a symlink to
/usr/include/cudd. With that, two brial-specific files, prefix.h and
prefix_internal.h need to be moved elsewhere, hence the new cuddaux
directory.

Afterwards, one will notice compile errors because PBORI_PREFIX is
undefined; this is because .cc files previously failed to include
prefix.h and relied on some implicit inclusion through another file
(not good), hereby fixed as well.

From there, one can abolish the symlink (again) and use an actual -I
argument to the compiler, editing "#include" lines as needed, and
offer the cudd include directory as a parameter through configure.ac.
@jengelh
Copy link
Contributor Author

jengelh commented Sep 10, 2020

I would prefer not to take any include directory if possible but test header presence and possibly library presence with AC_CHECK_HEADER and

implemented

The CI actually did run but failed

also addressed

does this work with recent versions of CUDD?

polybori/brial makes use cudd internal APIs (cuddInt.h) like

libbrial/include/polybori/cache/CCacheManagement.h:362:    PBORI_PREFIX(cuddCacheInsert2)(internalManager(), cache_dummy, first, second, result);
libbrial/include/polybori/routines/pbori_algo.h:749:  PBORI_PREFIX(cuddCacheInsert2)(table, pboriCuddZddUnionXor__, P, Q, res);

that are not meant to be public. cudd-2.5.0 erroneously installed cuddInt.h to /usr/include which may have led one to believe it's public. cudd-3.0.0 fixed that, cuddInt.h is no longer in /usr/include.

@kiwifb
Copy link
Member

kiwifb commented Sep 10, 2020

Still fighting to get travis showing on PR. Hope it will start working soon. Thanks for answering my question and concerns.

Do I understand that you still have to fix the use of stuff from cuddInt.h or have you fixed it?

@kiwifb
Copy link
Member

kiwifb commented Sep 10, 2020

CI looks good so far. OS X build still have to complete at the time of writing.
https://travis-ci.com/github/BRiAl/BRiAl/builds/183694463

@kiwifb
Copy link
Member

kiwifb commented Sep 10, 2020

Answering my own question after a bit of thought. This is limited to CUDD 2.5 .0 as you explicitly look for the header in question. This is annoying but clearly could be considered work for later.

@kiwifb
Copy link
Member

kiwifb commented Sep 11, 2020

This is good. But may need more work for an official release. This is clearly brial-2.0 material.

@kiwifb kiwifb merged commit 47f2a14 into BRiAl:master Sep 11, 2020
@kiwifb
Copy link
Member

kiwifb commented Oct 1, 2020

I very much neglected your two first lines before doing a release including this. "libbrial/include/polybori/cudd can be made into a symlink to /usr/include/cudd." this is clearly not acceptable for any package to be expected to do that kind of after install tweak. Moreover, it could interfere if you had cudd-3.0 installed since it would break your cudd install that brial cannot use.

kiwifb added a commit that referenced this pull request Oct 1, 2020
@jengelh
Copy link
Contributor Author

jengelh commented Oct 1, 2020

"libbrial/include/polybori/cudd can be made into a symlink to /usr/include/cudd." this is clearly not acceptable

I hope you read the commit message to the full extent, because it is just an intermediate thought state, ending in "From there, one can abolish the symlink (again)".

@kiwifb
Copy link
Member

kiwifb commented Oct 1, 2020

Yes, I have. And as it is, this is not ready to release, I had several thought after people said that you cannot compile against it out of the box. The easiest fix is of course to provide an extra -I flag. This would be relatively easy if we had a .pc file. But even then, this is awkward since it is only needed if internal cudd is used.

@kiwifb
Copy link
Member

kiwifb commented Oct 1, 2020

Note, that I ultimately want to re-include all of this but it may go into a dev branch until it is ready to be consumed in a more easy way downstream.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants