From fa3863f5a62c1078277eca72d1ca8cc0c4c9d62c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Tue, 26 Aug 2025 15:42:11 +0200 Subject: [PATCH 1/2] Clean up classifiers test --- .../captures/classifiers-secondclass.check | 39 +++++++++++ .../captures/classifiers-secondclass.scala | 70 +++++++++---------- 2 files changed, 71 insertions(+), 38 deletions(-) create mode 100644 tests/neg-custom-args/captures/classifiers-secondclass.check diff --git a/tests/neg-custom-args/captures/classifiers-secondclass.check b/tests/neg-custom-args/captures/classifiers-secondclass.check new file mode 100644 index 000000000000..af2c3e961658 --- /dev/null +++ b/tests/neg-custom-args/captures/classifiers-secondclass.check @@ -0,0 +1,39 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/classifiers-secondclass.scala:41:28 ---------------------- +41 | parReduce(1 to 1000): (a, b) => // error + | ^ + |Found: (a: Int, b: Int) ->{f.write, f.read} Int + |Required: (Int, Int) ->{cap.only[Read]} Int + | + |Note that capability f.write is not included in capture set {cap.only[Read]}. + | + |where: cap is a fresh root capability created in anonymous function of type (f²: Levels.File^): Unit when checking argument to parameter op of method parReduce +42 | f.write(42) // the error stems from here +43 | a + b + f.read() // ok + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/classifiers-secondclass.scala:53:30 ---------------------- +53 | parReduce(1 to 1000): (a, b) => // error + | ^ + |Found: (a: Int, b: Int) ->{f.write, f.read, g.read} Int + |Required: (Int, Int) ->{cap.only[Read]} Int + | + |Note that capability f.write is not included in capture set {cap.only[Read]}. + | + |where: cap is a fresh root capability created in anonymous function of type (g²: Levels.File^): Unit when checking argument to parameter op of method parReduce +54 | f.write(42) // the error stems from here +55 | a + b + f.read() + g.read() // ok + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/classifiers-secondclass.scala:56:30 ---------------------- +56 | parReduce(1 to 1000): (a, b) => // error + | ^ + |Found: (a: Int, b: Int) ->{g.write} Int + |Required: (Int, Int) ->{cap.only[Read]} Int + | + |Note that capability g.write is not included in capture set {cap.only[Read]}. + | + |where: cap is a fresh root capability created in anonymous function of type (g²: Levels.File^): Unit when checking argument to parameter op of method parReduce +57 | g.write(42) // the error stems from here +58 | 0 + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/classifiers-secondclass.scala b/tests/neg-custom-args/captures/classifiers-secondclass.scala index b631c9633cba..8fa2f386b526 100644 --- a/tests/neg-custom-args/captures/classifiers-secondclass.scala +++ b/tests/neg-custom-args/captures/classifiers-secondclass.scala @@ -1,24 +1,28 @@ import language.experimental.captureChecking import language.experimental.separationChecking +import language.experimental.erasedDefinitions + import caps.* // Test inspired by the "Gentrification Gone too Far?" paper object Levels: + /* User-defined capability classifiers */ trait Read extends Classifier, SharedCapability trait ReadWrite extends Classifier, SharedCapability trait File(val name: String): - val r: Read^ - val rw: ReadWrite^ - // operations guarded by boxed capability members + // file-specific capability members, these are ensured to be erased + erased val r: Read^ + erased val rw: ReadWrite^ + // operations guarded by capability members val read: () ->{r} Int val write: Int ->{rw} Unit object File: def apply(s: String): File^ = new File(s) { - val r = new Read {} - val rw = new ReadWrite {} + erased val r = new Read {} + erased val rw = new ReadWrite {} val read = () => println(s"Reading from $name with capability $r") 42 @@ -26,42 +30,32 @@ object Levels: println(s"Writing $i to $name with capability $rw") } - // Unfortunately, we do not have @use lambdas yet - trait UseFunction[U]: - def apply[C^](f: File^{C}): U - - def withFile[U](name: String)(block: UseFunction[U]): U = block(File(name)) // unrestricted use of files & other capabilities + def withFile[U](name: String)(block: File^ => U): U = block(File(name)) // unrestricted use of files & other capabilities def parReduce[U](xs: Seq[U])(op: (U, U) ->{cap.only[Read]} U): U = xs.reduce(op) // only Read-classified allowed @main def test = - withFile("foo.txt"): - new UseFunction[Unit]: - def apply[C^](f: File^{C}): Unit = - f.read() // ok - parReduce(1 to 1000): (a, b) => - a * b * f.read() // ok - parReduce(1 to 1000): (a, b) => // error - f.write(42) // the error stems from here - a + b + f.read() // ok - f.write(42) // ok, unrestricted access to file + withFile("foo.txt"): f => + f.read() // ok + parReduce(1 to 1000): (a, b) => + a * b * f.read() // ok + parReduce(1 to 1000): (a, b) => // error + f.write(42) // the error stems from here + a + b + f.read() // ok + f.write(42) // ok, unrestricted access to file def testMulti = - withFile("foo.txt"): - new UseFunction[Unit]: - def apply[C^](f: File^{C}): Unit = - withFile("bar.txt"): - new UseFunction[Unit]: - def apply[C^](g: File^{C}): Unit = - f.read() // ok - g.read() // ok - parReduce(1 to 1000): (a, b) => - a * b * f.read() + g.read() // ok - parReduce(1 to 1000): (a, b) => // error - f.write(42) // the error stems from here - a + b + f.read() + g.read() // ok - parReduce(1 to 1000): (a, b) => // error - g.write(42) // the error stems from here - 0 - f.write(42) // ok, unrestricted access to file - g.write(42) // ok, unrestricted access to file + withFile("foo.txt"): f => + withFile("bar.txt"): g => + f.read() // ok + g.read() // ok + parReduce(1 to 1000): (a, b) => + a * b * f.read() + g.read() // ok + parReduce(1 to 1000): (a, b) => // error + f.write(42) // the error stems from here + a + b + f.read() + g.read() // ok + parReduce(1 to 1000): (a, b) => // error + g.write(42) // the error stems from here + 0 + f.write(42) // ok, unrestricted access to file + g.write(42) // ok, unrestricted access to file From 6e6cf797e9a39a2998eec78b15a80a2906513e17 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Tue, 26 Aug 2025 17:00:49 +0200 Subject: [PATCH 2/2] Update 'How to Use the Capture Checker' --- .../capture-checking/how-to-use.md | 43 ++++++++++++++++++- 1 file changed, 42 insertions(+), 1 deletion(-) diff --git a/docs/_docs/reference/experimental/capture-checking/how-to-use.md b/docs/_docs/reference/experimental/capture-checking/how-to-use.md index e3bd2725ce73..834194322a34 100644 --- a/docs/_docs/reference/experimental/capture-checking/how-to-use.md +++ b/docs/_docs/reference/experimental/capture-checking/how-to-use.md @@ -6,7 +6,48 @@ nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-che ## Enabling Capture Checking -TODO +Use Scala 3 nightly for the latest features and fixes. + +Add this import in any file that uses capture checking: +```scala +import language.experimental.captureChecking +``` + +### Separation Checking + +Requires the import above: +```scala +import language.experimental.captureChecking +import language.experimental.separationChecking +``` + +### SBT Project Template + +Alternatively, you can clone a pre-defined SBT project to get +started: https://github.com/lampepfl/scala3-cc-template + +### The REPL/Scala-CLI + +Using the command line through explicit parameters: +```bash +scala -S 3.nightly -language:experimental.captureChecking +``` +or when reading from a file: +```scala +// foo.scala: +//> using scala 3.nightly +import language.experimental.captureChecking +... +``` +Then, it suffices to run +```bash +scala foo.scala +``` + +## API Documentation + +Scaladoc supports capture checking. The nightly standard library API docs have it enabled by default: +https://nightly.scala-lang.org/api/ ## Compilation Options