diff --git a/anneal/v1/playground/rust-anneal-playground/.dockerignore b/anneal/v1/playground/rust-anneal-playground/.dockerignore new file mode 100644 index 0000000000..954fb3c0a5 --- /dev/null +++ b/anneal/v1/playground/rust-anneal-playground/.dockerignore @@ -0,0 +1,14 @@ +# Keep root Docker/CI build contexts from sending local build artifacts. +.git +.DS_Store +**/.DS_Store + +target +**/target + +ui/target +ui/frontend/node_modules +ui/frontend/dist +ui/frontend/.cache +ui/frontend/.webpack +ui/tmp \ No newline at end of file diff --git a/anneal/v1/playground/rust-anneal-playground/CRATE_POLICY.md b/anneal/v1/playground/rust-anneal-playground/CRATE_POLICY.md new file mode 100644 index 0000000000..62383c5977 --- /dev/null +++ b/anneal/v1/playground/rust-anneal-playground/CRATE_POLICY.md @@ -0,0 +1,71 @@ +# Playground crate inclusion policy + +The playground selects a number of root crates to include: + +- The top 100 crates based on [all time downloads][] +- Crates from the [Rust cookbook][] + +A recent non-[prerelease][] version of these crates are available, as +well as whatever dependencies these crates require. + +Please do not open issues or pull requests about adding or updating +crates available in the playground. This list is maintained +semi-automatically and all crates are updated at once to reduce +duplicate work. The update frequency is sporadic, but usually +corresponds to when a new stable version of Rust is released: every +six weeks. + +## Why is there a policy? + +The number of crates must be restricted because time and space are +limited resources and the playground is a volunteer-supported open source +project. It would be infeasible to provide every possible crate. + +This inclusion policy is used to avoid "playing favorites" for which +crates are available. Hand-picking crates will lead to resentment +about which crates were not included between the playground +maintainers and crate authors or even the broader Rust community. +Neither of these outcomes is desired. + +## Exclusion policy + +Occasionally, some crates that would otherwise meet the above criteria +will not be available on the playground. A non-exhaustive list of +reasons is: + +- Does not compile on Linux +- Does not compile on the stable release channel +- Does not compile due to invalid feature flag selection + +In these cases, we will temporarily exclude the crate to allow the +playground to continue to be updated. We usually also notify the crate +maintainers so they can adjust their crates and be re-included. + +## I don't like the current system! + +We are open to well-reasoned [alternate algorithms][], but be aware +that any proposal would likely be expected to also provide the +majority of implementation work. + +## I am a crate author and I want to control which features are available + +When a crate is included in the playground, its Cargo.toml is +inspected for special metadata, similar to the [docs.rs +metadata][]. This will control what features we enable in addition to +the features needed by dependencies. + +```toml +[package] +name = "test" + +[package.metadata.playground] +default-features = true +features = ["std", "extra-traits"] +all-features = false +``` + +[prerelease]: https://semver.org/#spec-item-9 +[all time downloads]: https://crates.io/crates?sort=downloads +[Rust cookbook]: https://rust-lang-nursery.github.io/rust-cookbook/ +[alternate algorithms]: https://github.com/rust-lang/rust-playground/issues/101 +[docs.rs metadata]: https://docs.rs/about/metadata diff --git a/anneal/v1/playground/rust-anneal-playground/LICENSE-APACHE b/anneal/v1/playground/rust-anneal-playground/LICENSE-APACHE new file mode 100644 index 0000000000..9c8f3ea087 --- /dev/null +++ b/anneal/v1/playground/rust-anneal-playground/LICENSE-APACHE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "{}" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright {yyyy} {name of copyright owner} + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. \ No newline at end of file diff --git a/anneal/v1/playground/rust-anneal-playground/LICENSE-MIT b/anneal/v1/playground/rust-anneal-playground/LICENSE-MIT new file mode 100644 index 0000000000..9c5908c287 --- /dev/null +++ b/anneal/v1/playground/rust-anneal-playground/LICENSE-MIT @@ -0,0 +1,21 @@ +The MIT License (MIT) + +Copyright (c) 2016-2017 Jake Goulding + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/anneal/v1/playground/rust-anneal-playground/PERFORMANCE.md b/anneal/v1/playground/rust-anneal-playground/PERFORMANCE.md new file mode 100644 index 0000000000..84ad1c959f --- /dev/null +++ b/anneal/v1/playground/rust-anneal-playground/PERFORMANCE.md @@ -0,0 +1,338 @@ +# Anneal Playground Performance Notes + +## Goal + +Measure setup latency separately from steady-state verification cost. + +Current Docker image build measurements: + +```text +current_successful_build_ms: 426586 +current_successful_build_human: 7m 6.586s +immediate_cached_rebuild_ms: 1270 +immediate_cached_rebuild_human: 1.270s +``` + +The first number is the meaningful current compiler image build duration. The +second number is a Docker cache-hit rebuild. + +## Docker Image Build Measurement + +Run the stable compiler image build and keep the log: + +```sh +cd /root/rust-anneal-playground/compiler +CHANNELS_TO_BUILD=stable bash ./build.sh 2>&1 | tee /tmp/anneal-docker-build-current.log +``` + +Print only the duration number, in milliseconds: + +```sh +grep '\[anneal-build-timing\].*image=rust-stable.*event=finish' \ + /tmp/anneal-docker-build-current.log \ + | tail -n 1 \ + | sed -E 's/.*elapsed_ms=([0-9]+).*/\1/' +``` + +## First/Cold Anneal Verification Measurement + +Restart the backend first so the request is cold for this backend process. Then +run one Anneal Verify request in the browser against the tiny test workload. + +Current cold-run measurement from the VM: + +```text +cold_backend_total_ms: 32310 +cold_cargo_anneal_verify_ms: 31767 +cold_backend_overhead_ms: 543 +cold_success: true +``` + +Use a dedicated backend log: + +```sh +/tmp/playground-ui-cold.log +``` + +Print exactly two duration numbers from the first cold run, in milliseconds: + +```sh +grep '\[anneal-verify-timing\].*event=finish' /tmp/playground-ui-cold.log \ + | tail -n 1 \ + | sed -E 's/.*backend_total_ms=([0-9]+).*cargo_anneal_verify_ms=([0-9]+).*/\1 \2/' \ + | tr ' ' '\n' +``` + +Interpretation: + +```text +line 1: cold_backend_total_ms +line 2: cold_cargo_anneal_verify_ms +``` + +If the timing line says `cargo_anneal_verify_ms_found=false`, the backend did +run Anneal but did not see the inner command timing marker in stdout/stderr. +Rebuild the backend from a version where Anneal Verify is wrapped with the +`[anneal] verification succeeded in ... ms` marker. + +Then calculate: + +```text +cold_backend_overhead_ms = + cold_backend_total_ms - cold_cargo_anneal_verify_ms +``` + +## Warm Repeated Anneal Verification Measurement + +Warm repeated measurements should reuse one live WebSocket session so the first +request can absorb session/container setup effects and the following requests +show repeated verifier cost. The public WebSocket client can confirm real +verifier execution by requiring the inner `[anneal] verification ... ms` marker, +but exact backend totals still come from `/tmp/playground-ui-cold.log`. + +Current public WebSocket sequence from 2026-07-24: + +```text +run success client_total_ms cargo_anneal_verify_ms client_observed_overhead_ms marker_found +1 true 32352 31494 858 true +2 true 13078 12478 600 true +3 true 13019 12232 787 true +4 true 13017 12659 358 true +5 true 14022 13192 830 true +``` + +Use run 1 as the session setup/cold-in-session point. Runs 2-5 are the current +warm repeated sample: + +```text +warm_repeated_cargo_anneal_verify_ms: 12478, 12232, 12659, 13192 +warm_repeated_cargo_anneal_verify_avg_ms: 12640 +warm_repeated_client_total_avg_ms: 13284 +warm_repeated_client_observed_overhead_avg_ms: 644 +``` + +Because these totals were collected over the public WebSocket instead of by +reading the VM log directly, treat `client_total_ms` and +`client_observed_overhead_ms` as close proxies for backend totals, not the +authoritative `backend_total_ms` and `backend_overhead_ms` fields. + +To backfill exact backend fields for the same run window, SSH to the VM and run: + +```sh +grep '\[anneal-verify-timing\].*event=finish' /tmp/playground-ui-cold.log | tail -n 6 +``` + +## Inner Anneal Verify Phase Notes + +Existing `RUST_LOG=ui=info,orchestrator=info,cargo_anneal=trace` output already +shows several useful inner phases. In the five-run WebSocket sequence above: + +```text +phase run 1 warm runs 2-5 +Charon 250.57 ms avg 132.57 ms +Aeneas 361.80 ms avg 369.45 ms +Lake build 22.72 s avg 4.22 s +Unattributed / diagnostics about 8.16 s avg about 7.92 s +``` + +The biggest observed cold-in-session delta is Lake build: it drops from about +22.7s on run 1 to about 4.0-4.4s on warm repeats. Charon and Aeneas are not the +dominant costs for the tiny workload. The remaining warm cost is mostly outside +the currently timed Charon/Aeneas/Lake lines, so the next useful instrumentation +target is to split materialization, Lake build, and Lean diagnostics with +explicit timing inside patched `cargo-anneal`. + +## Stable Anneal Prewarm Experiment + +Set `PLAYGROUND_ANNEAL_PREWARM_STABLE=1` when starting the backend to run the +tiny Anneal workload once after the backend successfully binds its port. The +warmup keeps the warmed stable coordinator alive and hands it to the first +WebSocket session that connects, so the first user-visible Verify with Anneal +can test whether it gets the warm Lake path. + +The startup command should include: + +```sh +PLAYGROUND_ANNEAL_PREWARM_STABLE=1 +``` + +Useful log markers: + +```text +[anneal-prewarm] starting stable Anneal prewarm +[anneal-prewarm] stable Anneal prewarm finished +[anneal-prewarm] using prewarmed stable coordinator for WebSocket +``` + +If the browser connects before the startup prewarm finishes, the backend logs: + +```text +[anneal-prewarm] no prewarmed coordinator ready for WebSocket +``` + +For the experiment, wait until the `stable Anneal prewarm finished` line appears, +open a fresh browser tab, then run Verify with Anneal once against the tiny test +workload. Compare that first user-visible run's Lake build time against the +previous cold-ish Lake time (~20-21s) and warm Lake time (~3.8-4.2s). + +## Persistent Anneal Target Experiment + +Set `PLAYGROUND_ANNEAL_PERSISTENT_TARGET=1` when starting the backend to mount a +Docker named volume at `/playground/anneal-workspace/target/anneal` in each +compiler container. The volume name is channel-specific: + +```text +playground-anneal-target-stable +playground-anneal-target-beta +playground-anneal-target-nightly +``` + +The first run that creates an empty Docker named volume should initialize it +from the compiler image, so the baked `cargo_target` cache remains available. +Subsequent compiler containers can then reuse the runtime-generated Lean +workspace and `.lake` build output across backend and container restarts. + +Use it together with startup prewarm to test whether the hidden prewarm itself +becomes warm after a restart: + +```sh +PLAYGROUND_ANNEAL_PERSISTENT_TARGET=1 +PLAYGROUND_ANNEAL_PREWARM_STABLE=1 +``` + +Useful log marker: + +```text +[anneal-cache] mounting persistent Anneal target volume +``` + +Expected measurement: + +1. Start once with the persistent target enabled and let the stable prewarm + finish. The first prewarm may still pay the cold Lake cost if the volume was + empty. +2. Restart the backend with the same env vars. +3. The next startup prewarm should show a warm `lake build` time, roughly in the + same 4s band as the previous warm user-visible runs. + +To reset the stable-channel experiment: + +```sh +docker volume rm playground-anneal-target-stable +``` + +## Generated Lean Source Sync Experiment + +The patched `cargo-anneal` now syncs the fresh `lean.tmp` tree into the existing +`lean` tree instead of deleting `lean` and renaming `lean.tmp` over it. During +that sync, byte-identical files are left in place, stale files are removed, and +the top-level `.lake` directory is preserved. This should keep mtimes stable for +unchanged generated Lean files and test whether Lake can skip more work than the +current warm ~4s build. + +Useful log marker: + +```text +Syncing Lean directory took +``` + +Expected measurement after rebuilding the compiler image: + +1. Run the tiny Anneal workload once to populate the persistent target volume. +2. Run the same workload again without changing the source. +3. Compare the second run's `Syncing Lean directory took` and `lake build` + timings against the current warm baseline of ~3.8-4.0s for Lake. + +## Lake Lean Diagnostics Experiment + +Set `PLAYGROUND_ANNEAL_LAKE_LEAN_DIAGNOSTICS=1` when starting the backend to pass +an experimental diagnostics mode into the compiler container. In this mode, +patched `cargo-anneal` skips the standalone: + +```text +lake build Generated Anneal +``` + +and runs diagnostics through: + +```text +lake --old lean generated//.lean -- --json +``` + +The goal is to test whether Lake can build the imports needed for the spec and +emit JSON diagnostics in a single command, rather than paying both the warm +`lake build` cost (~4s) and a separate `lake env lean --json` diagnostics cost +(~6.2-6.5s). + +Useful log markers: + +```text +[anneal-lake-lean] skipping standalone 'lake build' +'lake --old lean -- --json' for +Lean diagnostics took +``` + +Expected measurement: + +1. Rebuild the stable compiler image. +2. Restart the backend with `PLAYGROUND_ANNEAL_LAKE_LEAN_DIAGNOSTICS=1`, + `PLAYGROUND_ANNEAL_PERSISTENT_TARGET=1`, and + `PLAYGROUND_ANNEAL_PREWARM_STABLE=1`. +3. Run the tiny Anneal workload twice without changing the source. +4. Compare total runtime and the `lake --old lean -- --json` timing against the + current warm baseline: ~4s Lake build plus ~6.2-6.5s diagnostics. + +The first version of this experiment used `lake lean` without `--old` and failed +quickly with `failed to remove output artifacts: permission denied`. That points +at Lake's non-old build mode trying to clean artifacts under the symlinked, +read-only prebuilt Aeneas package cache. + +## Build Specs / Skip Success Diagnostics Experiment + +Set `PLAYGROUND_ANNEAL_BUILD_SPECS_SKIP_SUCCESS_DIAGNOSTICS=1` when starting the +backend to keep the standalone `lake build` flow while making the successful path +avoid the separate JSON diagnostics pass. + +In this mode, patched `cargo-anneal` normalizes each generated spec module to +`Spec.lean` and adds it to +the Lake library roots before running: + +```text +lake build Generated Anneal +``` + +If that build succeeds, the specs have already been checked by Lean, so +`cargo-anneal` skips the later `lake env lean --json` diagnostics command. If +the Lake build fails, `cargo-anneal` still runs JSON diagnostics so playground +users get source-mapped error output instead of only a raw build failure. + +Useful log markers: + +```text +[anneal-fast-diagnostics] successful Lake build included Spec; skipping post-build JSON diagnostics +[anneal-fast-diagnostics] Lake build failed after including Spec; running JSON diagnostics +``` + +Expected measurement: + +1. Rebuild the stable compiler image. +2. Restart the backend with + `PLAYGROUND_ANNEAL_BUILD_SPECS_SKIP_SUCCESS_DIAGNOSTICS=1`, + `PLAYGROUND_ANNEAL_PERSISTENT_TARGET=1`, and + `PLAYGROUND_ANNEAL_PREWARM_STABLE=1`. +3. Run the tiny Anneal workload twice without changing the source. +4. Compare total runtime and `lake build` timing against the current warm + baseline of ~11.4-11.9s total, where ~6.2-6.5s is the post-build diagnostics + pass. + +## Test Workload + +```rust +/// ```anneal, unsafe(axiom) +/// ``` +pub unsafe fn anneal_warmup_identity(x: u32) -> u32 { + x +} + +fn main() {} +``` diff --git a/anneal/v1/playground/rust-anneal-playground/README.md b/anneal/v1/playground/rust-anneal-playground/README.md new file mode 100644 index 0000000000..b1552e0d65 --- /dev/null +++ b/anneal/v1/playground/rust-anneal-playground/README.md @@ -0,0 +1,135 @@ +# Rust Anneal Playground + +// TODO: Figure out where to put this: +## Workflow for making changes to the website: +cd ~/rust-anneal-playground +git pull +cd ui/frontend +pnpm build +cd .. +cargo build --release +sudo systemctl restart anneal-playground + +This is the home of the [Rust Playground][real], +also [hosted by Integer 32][us]. + +[real]: https://play.rust-lang.org/ +[us]: https://play.integer32.com/ + +## What's it do? + +The playground allows you to experiment with Rust before you install +it locally, or in any other case where you might not have the compiler +available. + +It has a number of features, including: + +1. A nice, unobtrusive editor with syntax highlighting. +1. The ability to compile in debug or release mode against the current + stable, beta, or nightly version of Rust. +1. The top 100 popular crates (ranked by all-time downloads), crates + that are part of the [Rust Cookbook][] and all of their + dependencies are available for use! +1. The ability to quickly load and save your code to a + GitHub [Gist][gist] and share it with your friends. +1. [rustfmt][] and [Clippy][clippy] can be run against the source code. +1. The ability to see the LLVM IR, assembly, or Rust MIR for the + source code. + +[Rust Cookbook]: https://rust-lang-nursery.github.io/rust-cookbook/ +[gist]: https://gist.github.com/ +[rustfmt]: https://github.com/rust-lang/rustfmt +[clippy]: https://github.com/rust-lang/rust-clippy + +## Architecture + +A [React][react] frontend communicates with an [Axum][axum] +backend. [Docker][docker] containers are used to provide the various +compilers and tools as well as to help isolate them. + +We hope that this frontend and backend stack is comfortable to +potential contributors! If you are interested in contributing, please +feel free to ask a question and we might even be able to point out +some useful resources. + +[react]: https://reactjs.org/ +[axum]: https://github.com/tokio-rs/axum +[docker]: https://www.docker.com/ + +## Resource Limits + +### Network + +There is no network connection between the compiler container and the +outside world. + +### Memory + +The amount of memory the compiler and resulting executable use is +limited by the container. + +### Execution Time + +The total compilation and execution time is limited by the container. + +### Disk + +This sandbox **does not** provide any disk space limits. It is +suggested to run the server such that the temp directory is a +space-limited. One bad actor may fill up this shared space, but it +should be cleaned when that request ends. + +## Security Hall of Fame + +A large set of thanks go to those individuals who have helped by +reporting security holes or other attack vectors against the +Playground. Each report helps us make the Playground better! + +* Preliminary sandbox testing (PID limit) by Stefan O'Rear. + +If you'd like to perform tests that you think might disrupt service of +the Playground, get in touch and we can create an isolated clone to +perform tests on! Once fixed, you can choose to be credited here. + +## Development + +### Build the UI +``` +cd ui/frontend +pnpm install +pnpm watch # Will rebuild and watch for changes +``` + +If you don't need the backend running because you are only making +basic HTML/CSS/JS changes, directly open in your browser the built +`ui/frontend/build/index.html`. + +### Build and run the server + +``` +cd ui +cargo run +``` + +There are some optional configuration parameters described in the +[ui README](./ui/README.md) which you may set in a `.env` file. The server will +run with no configuration, but in order to load and save gists a GitHub token +must be configured. + +### Build or download the containers +``` +cd compiler +./build.sh # If you want to test changes to the containers +./fetch.sh # If you just want the current playground +``` + +## Deployment + +* [Amazon EC2 (Ubuntu)](deployment/ubuntu.md) + +## License + +Licensed under either of + * Apache License, Version 2.0 ([LICENSE-APACHE](LICENSE-APACHE) or http://www.apache.org/licenses/LICENSE-2.0) + * MIT license ([LICENSE-MIT](LICENSE-MIT) or http://opensource.org/licenses/MIT) +at your option. diff --git a/anneal/v1/playground/rust-anneal-playground/SECURITY.md b/anneal/v1/playground/rust-anneal-playground/SECURITY.md new file mode 100644 index 0000000000..0de59e5d0d --- /dev/null +++ b/anneal/v1/playground/rust-anneal-playground/SECURITY.md @@ -0,0 +1,6 @@ +The Rust Playground follows the same security reporting procedures as +the main Rust organization. If you have found a vulnerability in the +Playground, please report it according to [the Rust security +policy][policy]. Thanks! + +[policy]: https://www.rust-lang.org/policies/security