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 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