Skip to main content
  • Home
  • Development
  • Documentation
  • Donate
  • Operational login
  • Browse the archive

swh logo
SoftwareHeritage
Software
Heritage
Archive
Features
  • Search

  • Downloads

  • Save code now

  • Add forge now

  • Help

https://github.com/EasyCrypt/easycrypt
16 March 2026, 10:24:02 UTC
  • Code
  • Branches (52)
  • Releases (9)
  • Visits
Revision 0dd57f714852f6f779d230c5bbf3e98e4594f41f authored by François Dupressoir on 06 December 2019, 09:55:55 UTC, committed by François Dupressoir on 06 December 2019, 09:55:55 UTC
OneMap-PRP: a PRP with a single map and lemmas to switch
This is to later support sampling the map eagerly, possibly
with programming queries as well.
1 parent a721392
  • Files
  • Changes
    • Branches
    • Releases
    • HEAD
    • refs/heads/aprhl
    • refs/heads/arrays
    • refs/heads/asynchile
    • refs/heads/bdep_ecCircuitsRefactor
    • refs/heads/bdep_merge_conseq_fix
    • refs/heads/bdep_mldsa_correctness
    • refs/heads/call-fwd-auto-frame
    • refs/heads/ci-build-docker-test-on-release
    • refs/heads/comm-algebra
    • refs/heads/copilot/fix-all-fixme-comments
    • refs/heads/coupling-rnd-tactics
    • refs/heads/delayed-couplings
    • refs/heads/deploy-fix-#154
    • refs/heads/deploy-quantum-upgrade
    • refs/heads/deploy-tc
    • refs/heads/distr-matrix
    • refs/heads/doc-seq-tactic
    • refs/heads/doc-types
    • refs/heads/doc-while-tactic
    • refs/heads/dynmatrix-stability
    • refs/heads/eHoare-example
    • refs/heads/eval-pwhile
    • refs/heads/expr-fold
    • refs/heads/feature_conseq_metavars
    • refs/heads/feature_procchange_framing
    • refs/heads/feature_signed_modP
    • refs/heads/fix-142
    • refs/heads/fix-729
    • refs/heads/fix_opsel_error_printing
    • refs/heads/fmap-fold
    • refs/heads/improve_nix_flake
    • refs/heads/indexed-types
    • refs/heads/jasmin-in-ci
    • refs/heads/latest
    • refs/heads/main
    • refs/heads/new-ehoare
    • refs/heads/ocaml-5
    • refs/heads/ois-refactoring
    • refs/heads/perms-group
    • refs/heads/polydiv
    • refs/heads/pose-match-fix
    • refs/heads/r2022.04-01
    • refs/heads/refactor_cfold
    • refs/heads/release
    • refs/heads/setoidrw
    • refs/heads/softcode-memories
    • refs/heads/subtypes
    • refs/heads/theory_finite_field
    • refs/heads/uptobad_warnings
    • refs/heads/vscode
    • refs/heads/yaeasypqc
    • refs/tags/r2024.09
    • 0dd57f714852f6f779d230c5bbf3e98e4594f41f
    • r2026.02
    • r2025.11
    • r2025.10
    • r2025.08
    • r2025.03
    • r2025.02
    • r2024.01
    • r2023.09
    • r2022.04
  • 0919a30
  • /
  • myocamlbuild.ml
Raw File Download Save again
Take a new snapshot of a software origin

If the archived software origin currently browsed is not synchronized with its upstream version (for instance when new commits have been issued), you can explicitly request Software Heritage to take a new snapshot of it.

Use the form below to proceed. Once a request has been submitted and accepted, it will be processed as soon as possible. You can then check its processing state by visiting this dedicated page.
swh spinner

Processing "take a new snapshot" request ...

To reference or cite the objects present in the Software Heritage archive, permalinks based on SoftWare Hash IDentifiers (SWHIDs) must be used.
Select below a type of object currently browsed in order to display its associated SWHID and permalink.

  • revision
  • directory
  • content
  • snapshot
origin badgerevision badge
swh:1:rev:0dd57f714852f6f779d230c5bbf3e98e4594f41f
origin badgedirectory badge
swh:1:dir:0919a30420498532a6e2059b46c400a1af42d619
origin badgecontent badge
swh:1:cnt:03a2635b3e8b3b9c27d0eca496e499cef05242b7
origin badgesnapshot badge
swh:1:snp:b6eeb0bcb674633e436c9d0fdc73d9fd939f58d3

This interface enables to generate software citations, provided that the root directory of browsed objects contains a citation.cff or codemeta.json file.
Select below a type of object currently browsed in order to generate citations for them.

  • revision
  • directory
  • content
  • snapshot
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Tip revision: 0dd57f714852f6f779d230c5bbf3e98e4594f41f authored by François Dupressoir on 06 December 2019, 09:55:55 UTC
OneMap-PRP: a PRP with a single map and lemmas to switch
Tip revision: 0dd57f7
myocamlbuild.ml
open Ocamlbuild_plugin

let _ = dispatch begin function
   | After_options ->
       Options.ocamlc   := S[!Options.ocamlc  ; A"-rectypes"];
       Options.ocamlopt := S[!Options.ocamlopt; A"-rectypes"];

   | After_rules ->
       (* Numerical warnings *)
       begin
         let wflag error mode wid =
           let mode = match mode with
             | `Enable  -> "+"
             | `Disable -> "-"
             | `Mark    -> "@"
           in
             match error with
             | false -> S[A"-w"; A(Printf.sprintf "%s%d" mode wid)]
             | true  -> S[A"-warn-error"; A(Printf.sprintf "%s%d" mode wid)]
         in
           for i = 1 to 59 do
             flag ["ocaml"; "compile"; Printf.sprintf "warn_+%d" i] & (wflag false `Enable  i);
             flag ["ocaml"; "compile"; Printf.sprintf "warn_-%d" i] & (wflag false `Disable i);
             flag ["ocaml"; "compile"; Printf.sprintf "warn_@%d" i] & (wflag false `Mark    i);
             flag ["ocaml"; "compile"; Printf.sprintf "werr_+%d" i] & (wflag true  `Enable  i);
             flag ["ocaml"; "compile"; Printf.sprintf "werr_-%d" i] & (wflag true  `Disable i);
             flag ["ocaml"; "compile"; Printf.sprintf "werr_@%d" i] & (wflag true  `Mark    i)
           done
       end;

       (* menhir & --explain/--trace/--table *)
       flag ["ocaml"; "parser"; "menhir"; "menhir_explain"] & A"--explain";
       flag ["ocaml"; "parser"; "menhir"; "menhir_trace"  ] & A"--trace";
       flag ["ocaml"; "parser"; "menhir"; "menhir_table"  ] & A"--table";

       (* Threads switches *)
       flag ["ocaml"; "pkg_threads"; "compile"] (S[A "-thread"]);
       flag ["ocaml"; "pkg_threads"; "link"] (S[A "-thread"]);

       (* Bisect *)
       flag ["ocaml"; "compile" ;  "bisect"] & S[A"-package"; A"bisect"];
       flag ["ocaml"; "compile" ;  "bisect"] & S[A"-syntax" ; A"camlp4o"];
       flag ["ocaml"; "compile" ;  "bisect"] & S[A"-syntax" ; A"bisect_pp"];
       flag ["ocaml"; "ocamldep";  "bisect"] & S[A"-package"; A"bisect"];
       flag ["ocaml"; "ocamldep";  "bisect"] & S[A"-syntax" ; A"camlp4o"];
       flag ["ocaml"; "ocamldep";  "bisect"] & S[A"-syntax" ; A"bisect_pp"];
       flag ["ocaml"; "link"    ;  "bisect"] & S[A"-package"; A"bisect"];

       (* Lint switches *)
       flag ["ocaml"; "lint"; "compile"] (S[A "-ppx"; A "../lint/ppx_lint.native"])

   | _ -> ()
end
The diff you're trying to view is too large. Only the first 1000 changed files have been loaded.
Showing with 0 additions and 0 deletions (0 / 0 diffs computed)
swh spinner

Computing file changes ...

back to top

Software Heritage — Copyright (C) 2015–2026, The Software Heritage developers. License: GNU AGPLv3+.
The source code of Software Heritage itself is available on our development forge.
The source code files archived by Software Heritage are available under their own copyright and licenses.
Terms of use: Archive access, API— Content policy— Contact— JavaScript license information— Web API