Variant submodule #4344

thk123 · 2019-03-07T14:06:53Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
[n/a] My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

This is a proposed replacement for #3962 that I hope might be less controversial. It provides the following advantages:

tests provided by the original repo are run in our CI
easy to find the source of variation

I didn't spend much time on this, so if people don't like it, no harm no fowl, but would quite like to be able to use variant.

martin-cs · 2019-03-07T14:17:33Z

src/util/variant.h

+/*******************************************************************\
+
+Module: typedef for optional class template. To be replaced with
+        std::optional once C++17 support is enabled


Should this be in 'nonstd/' with the existing optional code?

Since it is a submodule, I don't think I can change the namespace it is in? Or do you mean, making the using nostd::variantt = ... - the optionalt is declared in the global scope so I figured this was more consistent.

But your comment highlighted a copy-pasta error in the docs - fixed

Thinking about it; just a comment saying // Swap for std::variant when switching to C++17 or something.

Not sure I follow, comment currently reads (typo not withstanding):

To be replaced with std::variant once C++17 support is enabled

Is your suggestion your wording is clearer? Happy to change if that is indeed what you mean, but for me they are equivalent

Full tests are provided in the submodule - this checks that it compiles and links correctly.

thk123 · 2019-03-08T15:46:05Z

This is failing due to Makefile not linking the variant in util.

Before I spend some time figuring out how Makefiles work again, I would appreciate some indication from @tautschnig / @kroening / @peterschrammel as to whether this approach would be preferable or acceptable way of introducing a variant.

tautschnig · 2019-03-11T06:14:00Z

.gitmodules

@@ -1,3 +1,6 @@
 [submodule "jbmc/lib/java-models-library"]
 	path = jbmc/lib/java-models-library
 	url = https://github.com/diffblue/java-models-library.git
+[submodule "lib/variant"]


Instead of introducing a new top-level folder, can we place this in nonstd/variant instead of lib/variant?

tautschnig · 2019-03-11T06:15:24Z

scripts/run_variant_tests.sh

+cd lib/variant
+mkdir -p build
+cd build
+cmake -DMPARK_VARIANT_INCLUDE_TESTS="mpark" -DCMAKE_CXX_FLAGS="-std=c++11" ..


Are we sure that cmake is installed prior to running this (as this is being run in all Travis jobs)?

Hmm good point - what would you suggest - the project is in CMake not Make? (one option of course being: abandon this approach!)

I don't think there's a problem asking for cmake to be installed. Just make sure it's documented/actually done in CI configurations.

tautschnig · 2019-03-11T06:16:14Z

src/util/module_dependencies.txt

 nonstd
 sys # system
 util
+


tautschnig · 2019-03-11T06:20:00Z

src/util/variant.h

+#ifndef CPROVER_UTIL_VARIANT_H
+#define CPROVER_UTIL_VARIANT_H
+
+#include <mpark/variant.hpp>


I suppose this works with CMake, but shouldn't this be #include <lib/variant/mpark/variant.hpp>? If that, however, does not work with CMake then we'd need to update INCLUDES in any Makefile that wants to use this.

So only the util includes need to change, since all other users should use the variantt wrapper. But happy to do that if that's the preference.

Well, but the variant.h file uses this include, so if I'm in directory X and have a file x/y.cpp that includes variant.h then the preprocessor still needs to know how to resolve that include.

kroening · 2019-03-11T10:38:17Z

I am concerned about the following: so far, we have been able to build cbmc from a tarball (I am aware that this doesn't work with jbmc). We would now introduce a compile-time dependency on git, plus the ability to clone that repo.

peterschrammel · 2019-03-11T11:00:14Z

unit/util/variant.cpp

@@ -0,0 +1,12 @@
+// Copyright 2016-2019 Diffblue Limited. All Rights Reserved.


Wrong copyright header

smowton · 2019-03-11T11:45:17Z

@kroening subtree rather than submodule would fix that

thk123 · 2019-03-12T13:39:12Z

@kroening lmk if @smowton suggestion would work for you and I can swap this over to use a subtree.

peterschrammel · 2019-04-04T09:40:12Z

If dependency on a repo that is not under our control is considered a problem we could also fork it into the org.

we have been able to build cbmc from a tarball

Note that CBMC already now requires an extra step (minisat) to build it from a tarball - tracking https://github.com/niklasso/minisat (or a fork of it) through a submodule would be more convenient.

tautschnig · 2019-04-04T09:45:25Z

As a rather different suggestion: have people considered to just build using -std=c++17 and just use std::variant? That's not something we can realistically do for CBMC at the moment, but if the main interest in using variant is in downstream projects then those projects could just change their compiler requirements.

LAJW · 2019-04-04T09:59:57Z

just build using -std=c++17

I'd love that, and nothing technical is stopping us from doing so. But someone doesn't want that.

Nevertheless, availability of variant in CBMC wouldn't be a bad thing.

smowton · 2019-04-04T10:05:58Z

If you want a self-sufficient repo but also the ability to easily track what other-repo commit we're using, just subtree it. That would satisfy @kroening's concern

NlightNFotis · 2022-03-15T15:47:19Z

Closing this PR on the basis of:

Inactivity for about 3 years now.
Significant divergence from mainline (CI is very outdated and merge conflicts exist).

If you believe this has been in err, feel free to reopen the issue.

Add variant submodule

a9db042

thk123 requested review from tautschnig and kroening March 7, 2019 14:06

thk123 requested review from chrisr-diffblue, forejtv, peterschrammel, pkesseli and smowton as code owners March 7, 2019 14:06

thk123 mentioned this pull request Mar 7, 2019

add an implementation of std::variant<...> #3962

Closed

4 tasks

martin-cs reviewed Mar 7, 2019

View reviewed changes

thk123 force-pushed the variant-submodule branch from 3355d77 to f0db1cd Compare March 7, 2019 14:30

Run existing variant tests on travis

e3edd5c

thk123 force-pushed the variant-submodule branch from f0db1cd to dc49182 Compare March 8, 2019 14:16

Add basic unit test

8437b25

Full tests are provided in the submodule - this checks that it compiles and links correctly.

thk123 force-pushed the variant-submodule branch 3 times, most recently from cd81a6f to 8437b25 Compare March 8, 2019 15:44

tautschnig reviewed Mar 11, 2019

View reviewed changes

tautschnig assigned thk123 Mar 11, 2019

peterschrammel reviewed Mar 11, 2019

View reviewed changes

unit/util/variant.cpp

@@ -0,0 +1,12 @@

// Copyright 2016-2019 Diffblue Limited. All Rights Reserved.

Copy link

Member

peterschrammel Mar 11, 2019

Choose a reason for hiding this comment

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

Wrong copyright header

LAJW approved these changes Mar 11, 2019

View reviewed changes

NlightNFotis closed this Mar 15, 2022

		@@ -0,0 +1,12 @@
		// Copyright 2016-2019 Diffblue Limited. All Rights Reserved.

Variant submodule #4344

Variant submodule #4344

Uh oh!

Conversation

thk123 commented Mar 7, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thk123 Mar 7, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thk123 commented Mar 8, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented Mar 11, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton commented Mar 11, 2019

Uh oh!

thk123 commented Mar 12, 2019

Uh oh!

peterschrammel commented Apr 4, 2019

Uh oh!

tautschnig commented Apr 4, 2019

Uh oh!

LAJW commented Apr 4, 2019

Uh oh!

smowton commented Apr 4, 2019

Uh oh!

NlightNFotis commented Mar 15, 2022

Uh oh!

Uh oh!

thk123 Mar 7, 2019 •

edited

Loading