diff --git a/subprojects/docs/src/learn/docker/cli.md b/subprojects/docs/src/learn/docker/cli.md new file mode 100644 index 00000000..b03565a8 --- /dev/null +++ b/subprojects/docs/src/learn/docker/cli.md @@ -0,0 +1,160 @@ +--- +SPDX-FileCopyrightText: 2024 The Refinery Authors +SPDX-License-Identifier: EPL-2.0 +sidebar_position: 1 +sidebar_label: CLI +--- + +# Command-line interface + +You can run Refinery as a command-line applications via our [Docker container](https://github.com/graphs4value/refinery/pkgs/container/refinery-cli) on either `amd64` or `arm64` machines: + +```shell +docker run --rm -it -v ${PWD}:/data ghcr.io/graphs4value/refinery-cli:@@@tools.refinery.release@@@ +``` + +This will let you read input files and generate models in the current directory (`${PWD}`) of your terminal session. +Module imports (e.g., `import some::module.` to import `some/module.refinery`) relative to the current directory are also supported. + +For example, to generate a model based on the file named `input.problem` in the current directory and write the results into the file named `output.refinery`, you may run the [`generate` subcommand](#generate) with + +```shell +docker run --rm -it -v ${PWD}:/data ghcr.io/graphs4value/refinery-cli:@@@tools.refinery.release@@@ generate -o output.refinery input.problem +``` + +If you want Refinery CLI to print its documentation, run + +```shell +docker run --rm -it -v ${PWD}:/data ghcr.io/graphs4value/refinery-cli:@@@tools.refinery.release@@@ --help +``` + +## The `generate` subcommand {#generate} + +The `generate` subcommand generates a consistent concrete model from a partial model. + +```shell +docker run --rm -it -v ${PWD}:/data ghcr.io/graphs4value/refinery-cli:@@@tools.refinery.release@@@ generate [options] input path +``` + +The `input path` should be a path to a `.problem` file relative to the current directory. +Due to Docker containerization, paths _outside_ the current directory (e.g., `../input.problem`) are not supported. + +Passing `-` as the `input path` will read a partial model from the standard input. + +By default, the generator is _deterministic_ and always outputs the same concrete model. See the [`-random-seed`](#generate-random-seed) option to customize this behavior. + +See below for the list of supported `[options]`. + +### `-output`, `-o` {#generate-output} + +The output path for the generated model. +Passing `-o -` will write the generated model to the standard output. + +When generating multiple models with [`-solution-number`](#generate-solution-number), the value `-` is not supported and individual solutions will be saved to numbered files. +For example, if you pass `-o output.refinery -n 10`, solutions will be saved as `output_001.refinery`, `output_002.refinery`, ..., `output_010.refinery`. + +**Default value:** `-`, i.e., the solution is written to the standard output. + +### `-random-seed`, `-r` {#generate-random-seed} + +Random seed to control the behavior of model generation. + +The same random seed value and Refinery release will produce the same output model for an input problem. +Models generated with different values of `-random-seed` are highly likely (but are not guaranteed) to be _substantially_ different. + +**Default value:** `1` + +### `-scope`, `-s` {#generate-scope} + +Add [scope constraints](/learn/language/logic#type-scopes) to the input problem. + +This option is especially useful if you want to generate models of multiple sizes from the same partial model. + +For example, the command + +```shell +docker run --rm -it -v ${PWD}:/data ghcr.io/graphs4value/refinery-cli:@@@tools.refinery.release@@@ generate -s File=20..25 input.problem +``` + +is equivalent to appending + +```refinery title="input.problem" +scope File = 20..25. +``` + +to `input.problem`. +The syntax of the argument is equivalent to the [`scope`](/learn/language/logic#type-scopes) declaration, but you be careful with the handling of spaces in your shell. +Any number of `-s` arguments are supported. For example, the following argument lists are equivalent: + +```shell +-scope File=20..25,Directory=3 +-s File=20..25,Directory=3 +-s File=20..25 -s Directory=3 +-s "File = 20..25, Directory = 3" +-s "File = 20..25" -s "Directory = 3" +``` + +The `*` opeator also has to be quoted to avoid shell expansion: + +```shell +-s "File=20..*" +``` + +### `-scope-override`, `-S` {#generate-scope-override} + +Override [scope constraints](/learn/language/logic#type-scopes) to the input problem. + +This argument is similar to [`-scope`](#generate-scope), but has higher precedence than the [`scope`](/learn/language/logic#type-scopes) declarations already present in the input file. +However, you can't override `scope` declarations in modules imported in the input file using the `import` statement. + +For example, if we have + +```refinery title="input.problem" +scope File = 20..25, Directory = 3. +``` + +in the input file, the arguments `-s File=10..12 input.problem` will be interpreted as + +```refinery +scope File = 20..25, Directory = 3. +scope File = 10..12. +``` + +which results in an _unsatisfiable_ problem. If the use `-S File=10..12 input.problem` instead, the type scope for `File` is overridden as + +```refinery +scope Directory = 3. +scope File = 10..12. +``` + +and model generation can proceed as requested. Since we had specified no override for `Directory`, its type scope declared in `input.problem` was preserved. + +Scope overrides do not override additional scopes, i.e., `-s File=20..30 -S File=10..25` is interpreted as `-S File=20..25`. + +### `-solution-number`, `-n` {#generate-solution-number} + +The number of distinct solutions to generate. + +Generated solutions are always different, but are frequently not _substantially_ different, i.e., the differences between generated solutions comprise only a few model elements. +You'll likely generate substantially different models by calling the generator multiple times with different [`-random-seed`](#generate-random-seed) values instead. + +The generator will create [numbered output files](#generate-output) for each solution found. +The generation is considered successful if it finds at least one solution, but may find less than the requested number of solutions if no more exist. +In this case, there will be fewer output files than requested. + +**Default value:** `1` + +## Pre-release versions + +You can take advantage of the most recent code submitted to our repository by using the `latest` tag instead. + + +```shell +docker run --pull always --rm -it -v ${PWD}:/data ghcr.io/graphs4value/refinery-cli:latest +``` + +:::warning + +Pre-release versions may be unstable. + +::: diff --git a/subprojects/docs/src/learn/docker.md b/subprojects/docs/src/learn/docker/index.md similarity index 86% rename from subprojects/docs/src/learn/docker.md rename to subprojects/docs/src/learn/docker/index.md index d7604706..e7ab41eb 100644 --- a/subprojects/docs/src/learn/docker.md +++ b/subprojects/docs/src/learn/docker/index.md @@ -28,23 +28,14 @@ docker run --rm -it -p 8888:8888 ghcr.io/graphs4value/refinery:@@@tools.refinery Once Docker pulls and starts the container, you can navigate to http://localhost:8888 to open the model generation interface and start editing. -Alternatively, you can follow the [instructions to set up a local development environment](/develop/contributing) and compile and run Refinery from source. - -## Pre-release versions - -You can take advantage of the most recent code submitted to our repository by using the `latest` tag instead. - - -```shell -docker run --pull always --rm -it -p 8888:8888 ghcr.io/graphs4value/refinery:latest -``` +A [command-line interface (CLI)](cli) version of Refinery is also available as a Docker container. -Note that pre-release versions may be unstable. +Alternatively, you can follow the [instructions to set up a local development environment](/develop/contributing) and compile and run Refinery from source. ## Environmental variables The Docker container supports the following environmental variables to customize its behavior. -Customizing these variable should only be needed if you want to _increase resource limits_ or _expose you Refinery instance over the network_ for others. +Customizing these variables should only be needed if you want to _increase resource limits_ or _expose your Refinery instance over the network_ for others. Notes for **local-only instances** are highlighted with the :arrow_right: arrow emoji. @@ -128,21 +119,20 @@ Timeout for model generation in seconds. ### Threading -:warning: Excessively large values may overload the server. Make sure that _all_ Refinery threads can run at the same time to avoid thread starvation. +:arrow_right: If you only run a single model generation task at a time, you don't need to adjust these settings. + +:warning: Excessively large thread counts may overload the server. Make sure that _all_ Refinery threads can run at the same time to avoid thread starvation. #### `REFINERY_XTEXT_THREAD_COUNT` Number of threads used for non-blocking text editing operations. A value of `0` allows an _unlimited_ number of threads by running each semantics calculation in a new thread. -:warning: Excessively large values may overload the server. Make sure that _all_ Refinery threads can run at the same time to avoid thread starvation. - **Default value:** `1` #### `REFINERY_XTEXT_LOCKING_THREAD_COUNT` Number of threads used for text editing operations that lock the document. A value of `0` allows an _unlimited_ number of threads by running each semantics calculation in a new thread. - **Default value:** equal to `REFINERY_XTEXT_THREAD_COUNT` #### `REFINERY_XTEXT_SEMANTICS_THREAD_COUNT` @@ -151,15 +141,13 @@ Number of threads used for model semantics calculation. A value of `0` allows an Must be at least as large as `REFINERY_XTEXT_THREAD_COUNT`. -:warning: Excessively large values may overload the server. Make sure that _all_ Refinery threads can run at the same time to avoid thread starvation. - **Default value:** equal to `REFINERY_XTEXT_THREAD_COUNT` #### `REFINERY_MODEL_GENERATION_THREAD_COUNT` Number of threads used for model semantics calculation. A value of `0` allows an _unlimited_ number of threads by running each semantics calculation in a new thread. -:warning: Excessively large values may overload the server. Make sure that _all_ Refinery threads can run at the same time to avoid thread starvation. Each model generation task may also demand a large amount of memory in addition to CPU time. +:warning: Each model generation task may also demand a large amount of memory in addition to CPU time. **Default value:** equal to `REFINERY_XTEXT_THREAD_COUNT` @@ -171,6 +159,21 @@ Modules (`.refinery` files) in this directory or colon-separated list of directo :arrow_right: Use this in conjunction with the [mount volume (-v)](https://docs.docker.com/reference/cli/docker/container/run/#volume) option of `docker run` to work with multi-file projects in Refinery. -:warning: Make sure you only expose files that you want to make public. It's best to expose a directory that contains nothing other that `.refinery` files to minimize potential information leaks. +:warning: Only expose files that you want to make public. It's best to expose a directory that contains nothing other than `.refinery` files to minimize potential information leaks. **Default value:** _empty_ (no directories are exposed) + +## Pre-release versions + +You can take advantage of the most recent code submitted to our repository by using the `latest` tag instead. + + +```shell +docker run --pull always --rm -it -p 8888:8888 ghcr.io/graphs4value/refinery:latest +``` + +:::warning + +Pre-release versions may be unstable. + +:::