Skip to content

Commit

Permalink
Revert "Merge branch 'Golang/dev' into rishav-positional"
Browse files Browse the repository at this point in the history
This reverts commit 61d7284, reversing
changes made to 0a707a2.
  • Loading branch information
rishav-karanjit committed Sep 9, 2024
1 parent 61d7284 commit ca4d375
Show file tree
Hide file tree
Showing 456 changed files with 17,478 additions and 19,904 deletions.
4 changes: 0 additions & 4 deletions .github/workflows/manual.yml
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,3 @@ jobs:
uses: ./.github/workflows/test_models_python_tests.yml
with:
dafny: ${{ inputs.dafny }}
manual-ci-go:
uses: ./.github/workflows/test_models_go_tests.yml
with:
dafny: ${{ inputs.dafny }}
1 change: 0 additions & 1 deletion .github/workflows/nightly_dafny.yml
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,6 @@ jobs:
dafny-nightly-java,
dafny-nightly-net,
dafny-nightly-rust,
dafny-nightly-python,
]
if: ${{ always() && contains(needs.*.result, 'failure') }}
env:
Expand Down
29 changes: 2 additions & 27 deletions .github/workflows/pull.yml
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,10 @@ jobs:
steps:
- name: Populate Dafny versions list
id: populate-dafny-versions-list
run: echo "dafny-versions-list=['4.2.0', '4.4.0', '4.8.0']" >> $GITHUB_OUTPUT
run: echo "dafny-versions-list=['4.2.0', '4.4.0']" >> $GITHUB_OUTPUT
- name: Populate Dafny versions list for "only new versions" languages (Python)
id: populate-only-new-dafny-versions-list
run: echo "only-new-dafny-versions-list=['4.8.0']" >> $GITHUB_OUTPUT
run: echo "only-new-dafny-versions-list=['4.7.0']" >> $GITHUB_OUTPUT
outputs:
dafny-version-list: ${{ steps.populate-dafny-versions-list.outputs.dafny-versions-list }}
only-new-dafny-version-list: ${{ steps.populate-only-new-dafny-versions-list.outputs.only-new-dafny-versions-list }}
Expand Down Expand Up @@ -66,28 +66,3 @@ jobs:
uses: ./.github/workflows/test_models_python_tests.yml
with:
dafny: ${{ matrix.dafny-version }}
pr-ci-go:
needs: pr-populate-dafny-versions
strategy:
fail-fast: false
matrix:
dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.only-new-dafny-version-list) }}
uses: ./.github/workflows/test_models_go_tests.yml
with:
dafny: ${{ matrix.dafny-version }}

pr-ci-all-required:
if: always()
needs:
- pr-ci-verification
- pr-ci-java
- pr-ci-net
- pr-ci-rust
- pr-ci-python
- pr-ci-go
runs-on: ubuntu-latest
steps:
- name: Verify all required jobs passed
uses: re-actors/alls-green@release/v1
with:
jobs: ${{ toJSON(needs) }}
13 changes: 2 additions & 11 deletions .github/workflows/push.yml
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,10 @@ jobs:
steps:
- name: Populate Dafny versions list
id: populate-dafny-versions-list
run: echo "dafny-versions-list=['4.2.0', '4.4.0', '4.8.0']" >> $GITHUB_OUTPUT
run: echo "dafny-versions-list=['4.2.0', '4.4.0']" >> $GITHUB_OUTPUT
- name: Populate Dafny versions list for "only new versions" languages (Python)
id: populate-only-new-dafny-versions-list
run: echo "only-new-dafny-versions-list=['4.8.0']" >> $GITHUB_OUTPUT
run: echo "only-new-dafny-versions-list=['4.7.0']" >> $GITHUB_OUTPUT
outputs:
dafny-version-list: ${{ steps.populate-dafny-versions-list.outputs.dafny-versions-list }}
only-new-dafny-version-list: ${{ steps.populate-only-new-dafny-versions-list.outputs.only-new-dafny-versions-list }}
Expand Down Expand Up @@ -68,12 +68,3 @@ jobs:
uses: ./.github/workflows/test_models_python_tests.yml
with:
dafny: ${{ matrix.dafny-version }}
push-ci-go:
needs: pr-populate-dafny-versions
strategy:
fail-fast: false
matrix:
dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.only-new-dafny-version-list) }}
uses: ./.github/workflows/test_models_go_tests.yml
with:
dafny: ${{ matrix.dafny-version }}
162 changes: 88 additions & 74 deletions .github/workflows/test_models_go_tests.yml
Original file line number Diff line number Diff line change
@@ -1,64 +1,81 @@
name: Library Go tests

on:
workflow_call:
inputs:
dafny:
description: "The Dafny version to run"
required: true
type: string
num_shards:
required: false
type: number
default: 5
on: ["pull_request", "push"]

jobs:
populate-matrix-dimensions:
runs-on: ubuntu-latest
steps:
- name: Populate shard list
id: populate-shard-list
run: echo "shard-list=[`seq -s , 1 ${{ inputs.num_shards }}`]" >> $GITHUB_OUTPUT
outputs:
shard-list: ${{ steps.populate-shard-list.outputs.shard-list }}
testGo:
needs: populate-matrix-dimensions
test_go:
strategy:
fail-fast: false # at least for development; see all errors
fail-fast: false
matrix:
shard: ${{ fromJson(needs.populate-matrix-dimensions.outputs.shard-list) }}
runs-on: "ubuntu-latest"
permissions:
id-token: write
contents: read
env:
DOTNET_CLI_TELEMETRY_OPTOUT: 1
DOTNET_NOLOGO: 1
library: [
# TODO: Uncomment below before making PR
# TestModels/dafny-dependencies/StandardLibrary, # This stores current Polymorph dependencies that all TestModels depend on
TestModels/Aggregate,
# TestModels/AggregateReferences,
TestModels/CodegenPatches,
TestModels/Constraints,
TestModels/Constructor,
TestModels/Dependencies,
TestModels/Errors,
TestModels/Extendable,
TestModels/Extern,
# TestModels/LanguageSpecificLogic,
# TestModels/LocalService,
# TestModels/MultipleModels,
TestModels/Positional,
TestModels/Refinement,
TestModels/Resource,
# TestModels/SimpleTypes/BigDecimal,
# TestModels/SimpleTypes/BigInteger,
TestModels/SimpleTypes/SimpleBlob,
TestModels/SimpleTypes/SimpleBoolean,
# TestModels/SimpleTypes/SimpleByte,
TestModels/SimpleTypes/SimpleDouble,
TestModels/SimpleTypes/SimpleEnum,
# TestModels/SimpleTypes/SimpleEnumV2,
# TestModels/SimpleTypes/SimpleFloat,
TestModels/SimpleTypes/SimpleInteger,
TestModels/SimpleTypes/SimpleLong,
# TestModels/SimpleTypes/SimpleShort,
TestModels/SimpleTypes/SimpleString,
# TestModels/SimpleTypes/SimpleTimestamp,
TestModels/Union,
# TestModels/aws-sdks/ddb,
TestModels/aws-sdks/kms
]
runs-on: "macos-12"
steps:
- name: Support longpaths on Git checkout
run: |
git config --global core.longpaths true
- uses: actions/checkout@v2

- name: Configure AWS Credentials
uses: aws-actions/configure-aws-credentials@v1
# - name: Setup Dafny 4.5.0
# uses: dafny-lang/[email protected]
# with:
# dafny-version: 4.5.0
# TODO: Setup Dafny once its released
- name: Setup dotnet
uses: actions/setup-dotnet@v4
with:
aws-region: us-west-2
role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-PolymorphTestModels-Role-us-west-2
role-session-name: PythonTests
dotnet-version: 6.0.x

- uses: actions/checkout@v3
with:
submodules: recursive
- name: Build Dafny from source
run: |
git clone https://github.com/dafny-lang/dafny.git --recurse-submodules
cd dafny
make exe
- name: Install Z3 version 4.12.1
run: |
cd $GITHUB_WORKSPACE/dafny
make z3-mac
- name: Setup Dafny
uses: dafny-lang/[email protected]
with:
dafny-version: ${{ inputs.dafny }}
- name: Add Dafny to PATH
run: |
echo "$GITHUB_WORKSPACE/dafny/Scripts" >> $GITHUB_PATH
- name: Install Go
uses: actions/setup-go@v2
with:
go-version: "1.21"
go-version: '1.21'

- name: Install Go imports
run: |
Expand All @@ -67,36 +84,33 @@ jobs:
- name: Add go mod to Dafny Runtime Go
shell: bash
working-directory: ./DafnyRuntimeGo
run: |
run: |
go mod init github.com/dafny-lang/DafnyRuntimeGo
go mod tidy
- name: Setup Java 17 for codegen
uses: actions/setup-java@v3
with:
distribution: "corretto"
java-version: 17

- name: Setup smithy-dafny-conversion
uses: gradle/gradle-build-action@v2
with:
arguments: publishToMavenLocal
build-root-directory: smithy-dafny-conversion

- name: Install Smithy-Dafny codegen dependencies
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
- name: polymorph dafny dependencies
shell: bash
working-directory: ./TestModels/dafny-dependencies/StandardLibrary
run: |
export DAFNY_VERSION=4.6
make polymorph_dafny
make transpile_go
make polymorph_go
cd ./runtimes/go/ImplementationFromDafny-go/
go mod init github.com/dafny-lang/DafnyStandardLibGo
# TODO: This should handwritten (in the makefile or something)
echo "replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../DafnyRuntimeGo/" >> go.mod;
- name: Install smithy-dafny-codegen locally
uses: gradle/gradle-build-action@v2
with:
arguments: :smithy-dafny-codegen:pTML
build-root-directory: codegen
- name: Generate Polymorph Dafny and Go code
shell: bash
working-directory: ./${{ matrix.library }}
run: |
export DAFNY_VERSION=4.6
make polymorph_dafny
sh ./removeDotFromExtern.sh
make transpile_go
make polymorph_go
- name: Execute smithy-dafny-codegen-test tests
uses: gradle/gradle-build-action@v2
env:
JUNIT_SHARD: ${{ matrix.shard }}
JUNIT_SHARD_COUNT: ${{ inputs.num_shards }}
with:
arguments: :smithy-dafny-codegen-test:test --tests '*smithygo*' --info
build-root-directory: codegen
goimports -w runtimes/go/
cd runtimes/go/TestsFromDafny-go/
go run TestsFromDafny.go
2 changes: 1 addition & 1 deletion .github/workflows/test_models_rust_tests.yml
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ jobs:
- name: Set up Rust
uses: actions-rust-lang/setup-rust-toolchain@v1
with:
toolchain: "1.80.0"
toolchain: "1.76.0"
rustflags: ""
components: rustfmt

Expand Down
12 changes: 7 additions & 5 deletions SmithyDafnyMakefile.mk
Original file line number Diff line number Diff line change
Expand Up @@ -434,7 +434,7 @@ _polymorph_dafny: OUTPUT_DAFNY=\
--output-dafny $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(LIBRARY_ROOT)/Model)
_polymorph_dafny: INPUT_DAFNY=\
--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
_polymorph_dafny: _polymorph
_polymorph_dafny: _polymorph removeDots

# Generates dotnet code for all namespaces in this project
.PHONY: polymorph_dotnet
Expand Down Expand Up @@ -767,10 +767,6 @@ clean_go:
rm -rf $(LIBRARY_ROOT)/runtimes/go/ImplementationFromDafny-go
rm -rf $(LIBRARY_ROOT)/runtimes/go/TestsFromDafny-go

test_go:
cd runtimes/go/TestFromDafny-go
go run TestsFromDafny.go

########################## Python targets

# Python MUST transpile dependencies first to generate .dtr files
Expand Down Expand Up @@ -866,3 +862,9 @@ local_transpile_test_single: TRANSPILE_DEPENDENCIES= \
$(patsubst %, -library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX)) \
-library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
local_transpile_test_single: transpile_test

removeDots:
chmod +x ./removeDotFromExtern.sh
./removeDotFromExtern.sh

transpile_implementation_go: removeDots
80 changes: 0 additions & 80 deletions TestModels/Aggregate/runtimes/rust/src/standard_library_externs.rs

This file was deleted.

Loading

0 comments on commit ca4d375

Please sign in to comment.