From 67fc9ec448af3ed6a6203a3a0d00474f4486a075 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Wed, 22 Jan 2025 08:04:29 -0600 Subject: [PATCH] Chore: macosx unsupported for a performance file because inconsistent RC (#6062) By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .../IntegrationTests/TestFiles/LitTests/LitTest/README.md | 8 ++++++++ .../LitTests/LitTest/dafny0/CoinductiveProofs.dfy | 4 ++-- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md b/Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md index d630eb72a7b..be1c7db654c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md @@ -68,6 +68,14 @@ will be flagged by CI, and should be fixed by either converting it to use to flag it as intentionally inconsistent, for tests of backend-specific externs for example. +If a platform is not supported, please use the following command: + +``` +// UNSUPPORTED: windows, macosx +``` + +You can specify one or multiple platforms separated by a comma among `windows`, `posix`, `macosx` + ## Executing Tests from JetBrains Rider You will likely find it more convenient to run tests from an IDE such as diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy index f89bf98bb9d..6014efe5df7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy @@ -1,6 +1,6 @@ +// UNSUPPORTED: macosx +// Unsupported because the resource count is slightly different on macosx // RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation --performance-stats=1 - - codatatype Stream = Cons(head: T, tail: Stream) ghost function Upward(n: int): Stream