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

feat(TestModels): Resource #103

Merged
merged 47 commits into from
Feb 24, 2023
Merged

feat(TestModels): Resource #103

merged 47 commits into from
Feb 24, 2023

Commits on Jan 30, 2023

  1. test(resource): init testing of resource shim in C#

    Ran:
    git checkout smithy-test-models -- resources.smithy
    texastony committed Jan 30, 2023
    Configuration menu
    Copy the full SHA
    4a5d2c2 View commit details
    Browse the repository at this point in the history
  2. fix(resources): polymorph's smithydotnet does not handle bigInit or b…

    …igDecimal
    
    We may have to address this later.
    texastony committed Jan 30, 2023
    Configuration menu
    Copy the full SHA
    a74aaa9 View commit details
    Browse the repository at this point in the history

Commits on Jan 31, 2023

  1. feat: init Makefile for test

    Oi... this depends on all the simple types...
    Is that intentional?
    Or is that a mistake when we authored this Smithy?
    texastony committed Jan 31, 2023
    Configuration menu
    Copy the full SHA
    ee3e4b0 View commit details
    Browse the repository at this point in the history
  2. chore: ignore JetBrains

    texastony committed Jan 31, 2023
    Configuration menu
    Copy the full SHA
    df4a884 View commit details
    Browse the repository at this point in the history
  3. fix: resources.smithy

    Our Dafny code generator does not support:
    - Bytes
    - Shorts
    - Floats
    - BigInteger
    - BigDecimal
    - Timestamp
    texastony committed Jan 31, 2023
    Configuration menu
    Copy the full SHA
    e1b2cc3 View commit details
    Browse the repository at this point in the history
  4. fix: smithy-polymorph call's Model must be a directory

    Or smithy-polymorph will not output a Types.dfy.
    texastony committed Jan 31, 2023
    Configuration menu
    Copy the full SHA
    f144f7d View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    93d66b6 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    915e470 View commit details
    Browse the repository at this point in the history
  7. Configuration menu
    Copy the full SHA
    717ccd2 View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    19ff9bf View commit details
    Browse the repository at this point in the history
  9. Configuration menu
    Copy the full SHA
    9c0aee2 View commit details
    Browse the repository at this point in the history

Commits on Feb 1, 2023

  1. Configuration menu
    Copy the full SHA
    d7518c1 View commit details
    Browse the repository at this point in the history

Commits on Feb 2, 2023

  1. Configuration menu
    Copy the full SHA
    fa0c8d6 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    f495b3d View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    1af036c View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    4fd0bfc View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    e9060c4 View commit details
    Browse the repository at this point in the history
  6. feat: compile impl to C#

    texastony committed Feb 2, 2023
    Configuration menu
    Copy the full SHA
    6fa9de7 View commit details
    Browse the repository at this point in the history

Commits on Feb 3, 2023

  1. wip: test the implementation

    Issue: transpile_test_net is failing:
    
    ```
    $ make polymorph_dafny verify polymorph_net transpile_net
    dafny \
    	  -vcsCores:2 \
    	  -compileTarget:cs \
    	  -spillTargetCode:3 \
    	  -compile:0 \
    	  -optimizeErasableDatatypeWrapper:0 \
    	  -useRuntimeLib \
    	  -out runtimes/net/tests/TestsFromDafny \
    	  -library /Volumes/workplace/ryan-new-world/polymorph/TestModels/resources/src/Index.dfy \
    	  `find ./test -name '*.dfy'`
    Unhandled exception. System.AggregateException: One or more errors occurred. (Object reference not set to an instance of an object.)
     ---> System.NullReferenceException: Object reference not set to an instance of an object.
       at Microsoft.Dafny.ErrorReporter.Error(MessageSource source, IToken tok, String msg) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Reporting.cs:line 45
       at Microsoft.Dafny.ErrorReporter.Error(MessageSource source, IToken tok, String msg, Object[] args) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Reporting.cs:line 67
       at Microsoft.Dafny.Resolver.ResolveMember(IToken tok, Type receiverType, String memberName, NonProxyType& tentativeReceiverType) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 12384
       at Microsoft.Dafny.Resolver.EnsureSupportsErrorHandling(IToken tok, Type tp, Boolean expectExtract, Boolean hasKeywordToken) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 11884
       at Microsoft.Dafny.Resolver.ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext resolutionContext) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 11866
       at Microsoft.Dafny.Resolver.ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, ResolutionContext resolutionContext) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 11476
       at Microsoft.Dafny.Resolver.ResolveStatement(Statement stmt, ResolutionContext resolutionContext) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 9581
       at Microsoft.Dafny.Resolver.ResolveStatementWithLabels(Statement stmt, ResolutionContext resolutionContext) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 12132
       at Microsoft.Dafny.Resolver.ResolveBlockStatement(BlockStmt blockStmt, ResolutionContext resolutionContext) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 12102
       at Microsoft.Dafny.Resolver.ResolveMethod(Method m) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 8809
       at Microsoft.Dafny.Resolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 8001
       at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 2854
       at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 1043
       at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/Resolver/Resolver.cs:line 510
       at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/DafnyMain.cs:line 215
       at Microsoft.Dafny.Main.ParseCheck(IList`1 files, String programName, ErrorReporter reporter, Program& program) in /Volumes/workplace/dafny_src/dafny/Source/DafnyCore/DafnyMain.cs:line 166
       at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in /Volumes/workplace/dafny_src/dafny/Source/DafnyDriver/DafnyDriver.cs:line 345
       --- End of inner exception stack trace ---
       at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
       at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
       at System.Threading.Tasks.Task`1.get_Result()
       at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in /Volumes/workplace/dafny_src/dafny/Source/DafnyDriver/DafnyDriver.cs:line 123
       at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass10_0.<Main>b__0() in /Volumes/workplace/dafny_src/dafny/Source/DafnyDriver/DafnyDriver.cs:line 100
       at System.Threading.Thread.StartCallback()
    /Users/tonyknap/workplace/dafny_src/dafny_path/dafny: line 34: 15045 Abort trap: 6           "$DOTNET" "$DAFNY" "$@"
    make: *** [transpile_test_net] Error 134
    ```
    texastony committed Feb 3, 2023
    Configuration menu
    Copy the full SHA
    f073948 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    4e7cf00 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    9cd0b43 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    813dc9e View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    77b53ac View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    ba5b980 View commit details
    Browse the repository at this point in the history
  7. Configuration menu
    Copy the full SHA
    ca735c2 View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    d42449f View commit details
    Browse the repository at this point in the history
  9. Configuration menu
    Copy the full SHA
    e64a588 View commit details
    Browse the repository at this point in the history
  10. Configuration menu
    Copy the full SHA
    40ecc9a View commit details
    Browse the repository at this point in the history
  11. Configuration menu
    Copy the full SHA
    47d5e44 View commit details
    Browse the repository at this point in the history
  12. Configuration menu
    Copy the full SHA
    aa765c8 View commit details
    Browse the repository at this point in the history
  13. Configuration menu
    Copy the full SHA
    30fe621 View commit details
    Browse the repository at this point in the history
  14. wip: Test Wrapped Service

    `test_net` now fails with:
    ```
    /Volumes/workplace/ryan-new-world/polymorph/TestModels/resources/runtimes/net/Generated/Wrapped/TypeConversion.cs(190,13): error CS0246: The type or namespace name 'WrappedNativeWrapper_SimpleResource' could not be found (are you missing a using directive or an assembly reference?) [/Volumes/workplace/ryan-new-world/polymorph/TestModels/resources/runtimes/net/SimpleResources.csproj]
    ```
    
    Which I suspect is smithy-dotnet issue.
    It may be that smithy-dotnet assumes all resources
    are extendable.
    texastony committed Feb 3, 2023
    Configuration menu
    Copy the full SHA
    21db487 View commit details
    Browse the repository at this point in the history
  15. Configuration menu
    Copy the full SHA
    306cbaf View commit details
    Browse the repository at this point in the history
  16. Configuration menu
    Copy the full SHA
    fa49b2b View commit details
    Browse the repository at this point in the history

Commits on Feb 4, 2023

  1. Configuration menu
    Copy the full SHA
    70beb46 View commit details
    Browse the repository at this point in the history
  2. issue: WrappedCodegen's NativeWrapper assumes Exception name

    The C# Native Wrapper assumes an exception exsits
    named SimpleResourcesException.
    More generically,
    it assumes an exception named <Namespace>Exception exsits.
    
    Run:
    `make polymorph_dafny polymorph_net verify transpile_net setup_net test_net`
    to confirm.
    texastony committed Feb 4, 2023
    Configuration menu
    Copy the full SHA
    09aafe2 View commit details
    Browse the repository at this point in the history
  3. fix: issue in 09aafe2

    texastony committed Feb 4, 2023
    Configuration menu
    Copy the full SHA
    bbe673d View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    dc44957 View commit details
    Browse the repository at this point in the history

Commits on Feb 6, 2023

  1. style: run dotnet format

    texastony committed Feb 6, 2023
    Configuration menu
    Copy the full SHA
    6fdb22b View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2023

  1. feat(TestModels): Resource

    texastony committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    19493c3 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    6e4d07f View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    565ac6c View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    055a1ed View commit details
    Browse the repository at this point in the history
  5. refactor(TestModels): Resource

    Resolves PR #135 Feedback:
    - #135 (comment)
    texastony committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    be67a87 View commit details
    Browse the repository at this point in the history

Commits on Feb 23, 2023

  1. Configuration menu
    Copy the full SHA
    343c96f View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    fe10052 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    705ccb6 View commit details
    Browse the repository at this point in the history