-
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 (#1737)
Add js_of_ocaml build and deployment js_of_ocaml --enable=effects as per https://ocsigen.org/js_of_ocaml/latest/manual/tailcall and ocsigen/js_of_ocaml#1530 (comment) 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
2f79c57
commit 4915831
Showing
20 changed files
with
889 additions
and
38 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
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 |
|---|---|---|
|
|
@@ -7,7 +7,7 @@ | |
| bedrock2 clean-bedrock2 install-bedrock2 coqutil clean-coqutil install-coqutil \ | ||
| bedrock2-compiler clean-bedrock2-compiler install-bedrock2-compiler \ | ||
| rupicola clean-rupicola install-rupicola \ | ||
| util all-except-generated all \ | ||
| util all-except-generated all all-except-generated-and-js-of-ocaml all-except-js-of-ocaml \ | ||
| bedrock2-backend \ | ||
| deps \ | ||
| nobigmem print-nobigmem \ | ||
|
|
@@ -53,6 +53,7 @@ endif | |
| # coq .vo files that are not compiled using coq_makefile | ||
| SPECIAL_VOFILES := \ | ||
| src/ExtractionOCaml/%.vo \ | ||
| src/ExtractionJsOfOCaml/%.vo \ | ||
| src/ExtractionHaskell/%.vo \ | ||
| src/Rewriter/PerfTesting/Specific/generated/%.vo | ||
| GREP_EXCLUDE_SPECIAL := grep -v '^\(src/Extraction\(OCaml\|Haskell\)/\|src/Rewriter/PerfTesting/Specific/generated/\)' | ||
|
|
@@ -69,8 +70,10 @@ PERFTESTING_VO := \ | |
| src/Rewriter/PerfTesting/Core.vo \ | ||
| src/Rewriter/PerfTesting/StandaloneOCamlMain.vo | ||
| BEDROCK2_FILES_PATTERN := \ | ||
| src/ExtractionJsOfOCaml/bedrock2_% \ | ||
| src/ExtractionOCaml/bedrock2_% \ | ||
| src/ExtractionHaskell/bedrock2_% \ | ||
| src/ExtractionJsOfOCaml/with_bedrock2_% \ | ||
| src/ExtractionOCaml/with_bedrock2_% \ | ||
| src/ExtractionHaskell/with_bedrock2_% \ | ||
| src/Assembly/WithBedrock/% \ | ||
|
|
@@ -148,8 +151,10 @@ CHECK_OUTPUTS := $(addprefix check-,$(OUTPUT_PREOUTS)) | |
| ACCEPT_OUTPUTS := $(addprefix accept-,$(OUTPUT_PREOUTS) fiat-amd64.test) | ||
|
|
||
| all-except-compiled: coq pre-standalone-extracted check-output | ||
| all-except-generated: standalone-ocaml perf-standalone all-except-compiled | ||
| all: all-except-generated generated-files copy-to-fiat-rust copy-to-fiat-go | ||
| all-except-generated-and-js-of-ocaml: standalone-ocaml perf-standalone all-except-compiled | ||
| all-except-generated: all-except-generated-and-js-of-ocaml standalone-js-of-ocaml | ||
| all-except-js-of-ocaml: all-except-generated-and-js-of-ocaml generated-files | ||
| all: all-except-generated-and-js-of-ocaml standalone-js-of-ocaml generated-files copy-to-fiat-rust copy-to-fiat-go | ||
| @true | ||
| coq: $(REGULAR_VOFILES) | ||
| coq-without-bedrock2: $(REGULAR_EXCEPT_BEDROCK2_VOFILES) | ||
|
|
@@ -336,17 +341,25 @@ $(BEDROCK2_STANDALONE:%=src/ExtractionOCaml/%.ml): src/Bedrock/Standalone/Standa | |
| $(PERF_STANDALONE:%=src/ExtractionOCaml/%.ml): src/Rewriter/PerfTesting/StandaloneOCamlMain.vo | ||
| $(STANDALONE:%=src/ExtractionHaskell/%.hs): src/StandaloneHaskellMain.vo | ||
| $(BEDROCK2_STANDALONE:%=src/ExtractionHaskell/%.hs): src/Bedrock/Standalone/StandaloneHaskellMain.vo | ||
| $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.ml): src/StandaloneJsOfOCamlMain.vo | ||
| $(BEDROCK2_STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.ml): src/Bedrock/Standalone/StandaloneJsOfOCamlMain.vo | ||
| # $(PERF_STANDALONE:%=src/ExtractionHaskell/%.hs): src/Rewriter/PerfTesting/StandaloneHaskellMain.vo | ||
|
|
||
| pre-standalone-extracted: $(STANDALONE_OCAML:%=src/ExtractionOCaml/%.ml) $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%.hs) | ||
| pre-standalone-extracted: $(STANDALONE_OCAML:%=src/ExtractionOCaml/%.ml) $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.ml) $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%.hs) | ||
|
|
||
| $(STANDALONE_OCAML:%=src/ExtractionOCaml/%.ml) : %.ml : %.v | ||
| $(SHOW)'COQC $<' | ||
| $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< | ||
| $(HIDE)cat $*.tmp.ml | tr -d '\r' > $@ && rm $*.tmp.ml | ||
| $(HIDE)cat $*.tmp.mli | tr -d '\r' > $*.mli && rm $*.tmp.mli | ||
|
|
||
| $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%.hs) : %.hs : %.v src/haskell.sed | ||
| $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.ml) : %.ml : %.v | ||
| $(SHOW)'COQC $<' | ||
| $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< | ||
| $(HIDE)cat $*.tmp.ml | tr -d '\r' > $@ && rm $*.tmp.ml | ||
| $(HIDE)cat $*.tmp.mli | tr -d '\r' > $*.mli && rm $*.tmp.mli | ||
|
|
||
| $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%.hs) : %.hs : %.v src/haskell.sed src/StandaloneHaskellMain.vo | ||
| $(SHOW)'COQC $< > $@' | ||
| $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > [email protected] | ||
| $(HIDE)cat [email protected] | tr -d '\r' | sed -f src/haskell.sed > $@ && rm [email protected] | ||
|
|
||
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.