-
Notifications
You must be signed in to change notification settings - Fork 147
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add js_of_ocaml build and deployment
Some comparison of different arguments we could pass:
```
''
(real: 1247.15, user: 1237.92, sys: 8.82, mem: 3524544 ko)
--pretty --no-inline --debug-info --source-map
(real: 554.62, user: 545.29, sys: 9.31, mem: 4551068 ko)
--source-map --no-inline
(real: 431.91, user: 428.62, sys: 3.26, mem: 4588916 ko)
--source-map
(real: 599.19, user: 597.36, sys: 1.82, mem: 4528112 ko)
```
```
Time | Peak Mem | File Name
---------------------------------------------------------------------------
29m31.04s | 4582528 ko | Total Time / Peak Mem
---------------------------------------------------------------------------
10m11.06s | 4187496 ko | ExtractionJsOfOCaml/fiat_crypto.js
7m04.23s | 4582528 ko | ExtractionJsOfOCaml/bedrock2_fiat_crypto.js
7m03.61s | 4553728 ko | ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.js
1m23.70s | 2376368 ko | ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.ml
1m02.46s | 2376740 ko | ExtractionJsOfOCaml/bedrock2_fiat_crypto.ml
0m58.92s | 2324704 ko | ExtractionJsOfOCaml/fiat_crypto.ml
0m36.52s | 2840248 ko | ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.byte
0m30.87s | 2893620 ko | ExtractionJsOfOCaml/fiat_crypto.byte
0m30.58s | 2839784 ko | ExtractionJsOfOCaml/bedrock2_fiat_crypto.byte
0m02.66s | 1047220 ko | Bedrock/Standalone/StandaloneJsOfOCamlMain.vo
0m02.52s | 1014884 ko | StandaloneMonadicUtils.vo
0m02.30s | 1017460 ko | StandaloneJsOfOCamlMain.vo
0m00.61s | 103496 ko | ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.cmi
0m00.51s | 103272 ko | ExtractionJsOfOCaml/bedrock2_fiat_crypto.cmi
0m00.50s | 100760 ko | ExtractionJsOfOCaml/fiat_crypto.cmi
```- Loading branch information
1 parent
2177d3e
commit 8180d54
Showing
20 changed files
with
902 additions
and
49 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -56,7 +56,43 @@ jobs: | |
| coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} | ||
| ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} | ||
| export: CI ALLOW_DIFF COQCHKEXTRAFLAGS | ||
| custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 all-except-generated | ||
| custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 all-except-generated-and-js-of-ocaml | ||
| - name: standalone-js-of-ocaml | ||
| uses: coq-community/docker-coq-action@v1 | ||
| with: | ||
| coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} | ||
| ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} | ||
| export: CI ALLOW_DIFF COQCHKEXTRAFLAGS | ||
| custom_script: | | ||
| eval $(opam env) | ||
| opam install -y js_of_ocaml | ||
| etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 standalone-js-of-ocaml | ||
| - name: install-standalone-js-of-ocaml | ||
| run: make -f Makefile.standalone install-standalone-js-of-ocaml | ||
| - name: backup .gitignore | ||
| run: mv .gitignore{,.bak} | ||
| - name: Deploy js_of_ocaml 🚀 ${{ ( github.ref != 'refs/heads/master' && '(dry run)' ) || '' }} | ||
| uses: JamesIves/[email protected] | ||
| with: | ||
| branch: gh-pages # The branch the action should deploy to. | ||
| folder: fiat-html # The folder the action should deploy. | ||
| git-config-email: [email protected] | ||
| target-folder: . | ||
| single-commit: true # otherwise the repo will get too big | ||
| dry-run: ${{ github.ref != 'refs/heads/master' }} | ||
| - name: restore .gitignore | ||
| run: mv .gitignore{.bak,} | ||
| - name: upload standalone js files | ||
| uses: actions/upload-artifact@v3 | ||
| with: | ||
| name: standalone-html-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }} | ||
| path: fiat-html | ||
| - name: upload js_of_ocaml files | ||
| uses: actions/upload-artifact@v3 | ||
| with: | ||
| name: ExtractionJsOfOCaml-${{ matrix.env.COQ_VERSION }} | ||
| path: src/ExtractionJsOfOCaml | ||
| if: always () | ||
| - name: generated-files | ||
| run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -f Makefile.examples -j2 generated-files | ||
| if: github.event_name == 'pull_request' || ${{ matrix.env.COQ_VERSION }} != 'master' | ||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.