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.

Sign up for GitHub

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

Update dependency: deps/k_release #534

Merged
merged 36 commits into from
Mar 24, 2024
Merged

Update dependency: deps/k_release #534

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
36 commits
Select commit Hold shift + click to select a range
2f94fd2
deps/k_release: Set Version 6.3.24
Mar 1, 2024
df705ce
deps/k_release: Set Version 6.3.25
Mar 4, 2024
642982f
Merge remote-tracking branch 'origin/main' into _update-deps/runtimev…
Mar 6, 2024
fd993f2
deps/k_release: Set Version 6.3.28
Mar 6, 2024
ad682e3
Merge remote-tracking branch 'origin/main' into _update-deps/runtimev…
Mar 7, 2024
a339f23
deps/k_release: Set Version 6.3.29
Mar 7, 2024
65c0830
Merge remote-tracking branch 'origin/main' into _update-deps/runtimev…
Mar 13, 2024
73db86b
deps/k_release: Set Version 6.3.30
Mar 13, 2024
ae5a1bb
deps/k_release: Set Version 6.3.32
Mar 13, 2024
325798e
deps/k_release: Set Version 6.3.33
Mar 13, 2024
03ee464
deps/k_release: Set Version 6.3.34
Mar 13, 2024
d9331d2
deps/k_release: Set Version 6.3.35
Mar 13, 2024
975393b
deps/k_release: Set Version 6.3.37
Mar 13, 2024
40f93d5
Merge remote-tracking branch 'origin/main' into _update-deps/runtimev…
Mar 14, 2024
32c540d
deps/k_release: Set Version 6.3.39
Mar 14, 2024
023fe03
deps/k_release: Set Version 6.3.41
Mar 15, 2024
2b902e9
deps/k_release: Set Version 6.3.42
Mar 15, 2024
34d9914
deps/k_release: Set Version 6.3.43
Mar 18, 2024
d872cf5
deps/k_release: Set Version 6.3.44
Mar 18, 2024
4f562fb
deps/k_release: Set Version 6.3.45
Mar 19, 2024
f124445
deps/k_release: Set Version 6.3.47
Mar 20, 2024
03f57ea
deps/k_release: Set Version 6.3.50
Mar 20, 2024
38c6c5e
deps/k_release: Set Version 6.3.51
Mar 20, 2024
279e6a9
Merge branch 'main' into _update-deps/runtimeverification/k
rv-jenkins Mar 21, 2024
f68f6df
Merge branch 'main' into _update-deps/runtimeverification/k
rv-jenkins Mar 21, 2024
f987562
deps/k_release: Set Version 6.3.52
Mar 21, 2024
889f1b3
deps/k_release: Set Version 6.3.54
Mar 21, 2024
b45b942
update blockchain plugin, bump K dependency to latest
jberthold Mar 21, 2024
49739f9
shoe-horn the secp256k1 dependency into the foundry test setup
jberthold Mar 22, 2024
2ce8060
deps/k_release: Set Version 6.3.58
Mar 22, 2024
5bf5c25
make runDirectoryTest abort when the server does not start
jberthold Mar 22, 2024
1622515
modify how blake2 is included in foundry dylib
jberthold Mar 22, 2024
2aa77ff
follow name change for #if_#then_#else_#fi. Very important!
jberthold Mar 22, 2024
699cb55
TEMPORARY use fixed blockchain plugin from branch
jberthold Mar 22, 2024
873c7fb
Merge remote-tracking branch 'origin/main' into _update-deps/runtimev…
jberthold Mar 24, 2024
8f369e9
use blockchain-k-plugin from master
jberthold Mar 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion deps/blockchain-k-plugin_release
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
f27c5ec4861272c1ad4496bc6aab9f47dd6d473a
5aa6993fab90675d971b8b98b3430d11f1ec2a2b
2 changes: 1 addition & 1 deletion deps/k_release
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
6.3.23
6.3.58
2 changes: 2 additions & 0 deletions scripts/integration-tests.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,8 @@ cabal test llvm-integration

# The runDirectoryTest.sh script expects the following env vars to be set
export PLUGIN_DIR=$(nix build github:runtimeverification/blockchain-k-plugin/$PLUGIN_VERSION --no-link --json | jq -r '.[].outputs | to_entries[].value')
export SECP256K1_DIR=$(nix build nixpkgs#secp256k1 --no-link --json | jq -r '.[].outputs | to_entries[].value')
Copy link
Member

@jberthold jberthold Mar 22, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

This seems to be necessary now... root cause is that we don't actually get a linkable plugin library from including the blockchain-k-plugin, we rather get the sources and have to build things ourselves.
Also see the change to the plugin build and derivation for context.


cabal build all
KORE_RPC_BOOSTER=$(cabal exec which kore-rpc-booster)
BOOSTER_DEV=$(cabal exec which booster-dev)
Expand Down
12 changes: 7 additions & 5 deletions test/rpc-integration/resources/foundry-bug-report.kompile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,22 +2,24 @@ set -eux

SCRIPT_DIR=$(dirname $0)
PLUGIN_DIR=${PLUGIN_DIR:-""}

SECP=${SECP256K1_DIR:-/usr}

if [ -z "$PLUGIN_DIR" ]; then
echo "PLUGIN_DIR required to link in a crypto plugin dependency"
exit 1
else
for lib in libff libcryptopp libsecp256k1; do
for lib in libff libcryptopp blake2; do
LIBFILE=$(find ${PLUGIN_DIR} -name "${lib}.a" | head -1)
[ -z "$LIBFILE" ] && (echo "[Error] Unable to locate ${lib}.a"; exit 1)
PLUGIN_LIBS+="$LIBFILE "
PLUGIN_INCLUDE+="-I$(dirname $LIBFILE)/../include "
PLUGIN_INCLUDE+="-I$(dirname $LIBFILE) -I$(dirname $LIBFILE)/../include "
done
#PLUGIN_CPP=$(find ${PLUGIN_DIR}/plugin-c -name "*.cpp")
PLUGIN_CPP="${PLUGIN_DIR}/include/plugin-c/blake2.cpp ${PLUGIN_DIR}/include/plugin-c/crypto.cpp ${PLUGIN_DIR}/include/plugin-c/plugin_util.cpp"
PLUGIN_CPP="${PLUGIN_DIR}/include/plugin-c/crypto.cpp ${PLUGIN_DIR}/include/plugin-c/plugin_util.cpp"
fi

SECP_OPTS="-I${SECP}/include -L${SECP}/lib"

NAME=$(basename ${0%.tar.gz.kompile})
NAMETGZ=$(basename ${0%.kompile})

Expand All @@ -39,7 +41,7 @@ esac
llvm-kompile foundry-bug-report.llvm.kore ./dt c -- \
-fPIC -std=c++17 -o interpreter \
$PLUGIN_LIBS $PLUGIN_INCLUDE $PLUGIN_CPP \
-lcrypto -lssl $LPROCPS
-lcrypto -lssl $LPROCPS ${SECP_OPTS}
mv interpreter.* foundry-bug-report.dylib

# remove temporary artefacts
Expand Down
8 changes: 7 additions & 1 deletion test/rpc-integration/runDirectoryTest.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,13 @@ done

# find server port via lsof
server_port=$(lsof -a -p${server_pid} -sTCP:LISTEN -iTCP | grep ${server_pid} | sed -e 's/.* TCP \*:\([0-9]*\).*$/\1/')
echo "Server listening on port ${server_port}"

if [ -z "${server_port}" ]; then
echo "Unable to identify the server, aborting"
exit 4
else
echo "Server listening on port ${server_port}"
fi
Comment on lines +88 to +94
Copy link
Member

Choose a reason for hiding this comment

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

Previously we would happily continue with an empty server_port variable (garbling the rpc client command).


client="$client -p ${server_port}"

Expand Down
6 changes: 3 additions & 3 deletions test/rpc-integration/test-simplify/response-if-then-else-arity-error.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
"args": [
{
"tag": "App",
"name": "Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort",
"name": "Lblite",
Copy link
Member

Choose a reason for hiding this comment

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

This, of course, is a very important name change...

"sorts": [
{
"tag": "SortApp",
Expand Down Expand Up @@ -62,7 +62,7 @@
"context": [
{
"tag": "App",
"name": "Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort",
"name": "Lblite",
"sorts": [
{
"tag": "SortApp",
Expand Down Expand Up @@ -92,7 +92,7 @@
]
}
],
"error": "Inconsistent pattern. Symbol 'Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort' expected 3 arguments but got 2"
"error": "Inconsistent pattern. Symbol 'Lblite' expected 3 arguments but got 2"
}
],
"message": "Could not verify pattern"
Expand Down
2 changes: 1 addition & 1 deletion test/rpc-integration/test-simplify/response-if-then-else-indeterminate.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@
"args": [
{
"tag": "App",
"name": "Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort",
"name": "Lblite",
"sorts": [
{
"tag": "SortApp",
Expand Down
2 changes: 1 addition & 1 deletion test/rpc-integration/test-simplify/response-if-then-else-sort-error.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
"args": [
{
"tag": "App",
"name": "Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort",
"name": "Lblite",
"sorts": [
{
"tag": "SortApp",
Expand Down
2 changes: 1 addition & 1 deletion test/rpc-integration/test-simplify/state-if-then-else-arity-error.simplify
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@
"args": [
{
"tag": "App",
"name": "Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort",
"name": "Lblite",
"sorts": [
{
"tag": "SortApp",
Expand Down
2 changes: 1 addition & 1 deletion test/rpc-integration/test-simplify/state-if-then-else-eval.simplify
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@
"args": [
{
"tag": "App",
"name": "Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort",
"name": "Lblite",
"sorts": [
{
"tag": "SortApp",
Expand Down
2 changes: 1 addition & 1 deletion test/rpc-integration/test-simplify/state-if-then-else-false.simplify
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@
"args": [
{
"tag": "App",
"name": "Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort",
"name": "Lblite",
"sorts": [
{
"tag": "SortApp",
Expand Down
2 changes: 1 addition & 1 deletion test/rpc-integration/test-simplify/state-if-then-else-indeterminate.simplify
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@
"args": [
{
"tag": "App",
"name": "Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort",
"name": "Lblite",
"sorts": [
{
"tag": "SortApp",
Expand Down
2 changes: 1 addition & 1 deletion test/rpc-integration/test-simplify/state-if-then-else-sort-error.simplify
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@
"args": [
{
"tag": "App",
"name": "Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort",
"name": "Lblite",
"sorts": [
{
"tag": "SortApp",
Expand Down
2 changes: 1 addition & 1 deletion test/rpc-integration/test-simplify/state-if-then-else-true.simplify
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@
"args": [
{
"tag": "App",
"name": "Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort",
"name": "Lblite",
"sorts": [
{
"tag": "SortApp",
Expand Down