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

Revision a214a56a8d138704b1bb1f4390e61554b71b58e7 authored by Pierre-Yves Strub on 11 September 2023, 14:24:03 UTC, committed by Pierre-Yves Strub on 26 September 2023, 11:14:56 UTC
opsem: generate spec lemmas
1 parent 5e383f5
  • Files
  • Changes
  • 86bf3e2
  • /
  • Makefile
Raw File Download

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
revision badge
swh:1:rev:a214a56a8d138704b1bb1f4390e61554b71b58e7
directory badge
swh:1:dir:86bf3e27fcfca74c813cabae367c865caa77a5f7
content badge
swh:1:cnt:2f39dd618b94df6c72b4032fca864da380e00f84

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
(requires biblatex-software package)
Generating citation ...
(requires biblatex-software package)
Generating citation ...
(requires biblatex-software package)
Generating citation ...
Makefile
# -*- Makefile -*-

# --------------------------------------------------------------------
DUNE      ?= dune
ECARGS    ?=
ECTOUT    ?= 10
ECJOBS    ?= 0
ECEXTRA   ?= --report=report.log
ECPROVERS ?= Alt-Ergo Z3 CVC4
CHECKPY   ?=
CHECK     := $(CHECKPY) scripts/testing/runtest
CHECK     += --bin=./ec.native --bin-args="$(ECARGS)"
CHECK     += --bin-args="$(ECPROVERS:%=-p %)"
CHECK     += --timeout="$(ECTOUT)" --jobs="$(ECJOBS)"
CHECK     += $(ECEXTRA) config/tests.config

# --------------------------------------------------------------------
UNAME_P = $(shell uname -p)
UNAME_S = $(shell uname -s)

# --------------------------------------------------------------------
.PHONY: default build byte native tests check examples
.PHONY: clean install uninstall

default: build
	@true

build:
	rm -f src/ec.exe ec.native
	dune build -p easycrypt
	ln -sf src/ec.exe ec.native
ifeq ($(UNAME_P)-$(UNAME_S),arm-Darwin)
	-codesign -f -s - src/ec.exe
endif

install: build
	$(DUNE) install

uninstall:
	$(DUNE) uninstall

check: stdlib examples

stdlib: build
	$(CHECK) prelude stdlib

examples: build
	$(CHECK) examples mee-cbc

check: stdlib examples
	@true

clean:
	rm -f ec.native && $(DUNE) clean
	find theories examples -name '*.eco' -exec rm '{}' ';'

clean_eco:
	find theories examples -name '*.eco' -exec rm '{}' ';'
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