diff --git a/.github/workflows/publish.yml b/.github/workflows/publish.yml new file mode 100644 index 0000000..1615927 --- /dev/null +++ b/.github/workflows/publish.yml @@ -0,0 +1,43 @@ +name: Publish web +on: + push: + +jobs: + build: + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Setup Pages + id: pages + uses: actions/configure-pages@v3 + + - name: Install pandoc + run: | + sudo apt-get install --yes pandoc + + - name: Build with Pandoc + run: | + make + + - name: Upload artifact + uses: actions/upload-pages-artifact@v5 + + deploy: + permissions: + contents: read + pages: write + id-token: write + + runs-on: ubuntu-latest + + needs: build + + environment: + name: github-pages + url: ${{steps.deployment.outputs.page_url}} + steps: + - name: Deploy artifact + id: deployment + uses: actions/deploy-pages@v5 diff --git a/Makefile b/Makefile index d19756f..b41abbd 100644 --- a/Makefile +++ b/Makefile @@ -1,21 +1,26 @@ -MAP=map -OUT=html -TEMPLATE=tpl/default +.PHONY: all -include Makefile.base +all: _site/about.html \ + _site/contact.html \ + _site/documentation.html \ + _site/download.html \ + _site/home.html \ + _site/index.html -publish: all - git add . - git stash - git checkout master - git checkout --theirs stash -- . - git stash drop - git reset . - git clean -df - git clean -df +_site/about.html: about.md + ./compile.sh About $< default -home.html: home.nav home.content tpl/home - web-render tpl/home home home.nav home.content > $@ +_site/contact.html: contact.md + ./compile.sh Contact $< default -index.html: home.html - ln -s $< $@ +_site/documentation.html: documentation.md + ./compile.sh Documentation $< default + +_site/download.html: download.md + ./compile.sh Download $< default + +_site/home.html: home.md + ./compile.sh Home $< home + +_site/index.html: _site/home.html + cp $< $@ diff --git a/Makefile.base b/Makefile.base deleted file mode 100644 index 34572e4..0000000 --- a/Makefile.base +++ /dev/null @@ -1,19 +0,0 @@ -HTML=$(shell awk '$$1 == "T" {print $$2}' $(MAP)) - -all: $(HTML) - -%.nav: $(MAP) - web-nav $^ | markdown > $@ - -%.content: %.md - markdown $^ > $@ - -%.html: %.nav %.content $(TEMPLATE) - web-render $(TEMPLATE) $* $*.nav $*.content > $@ - -clean: - rm -f $(HTML) - rm -f $(HTML:.html=.nav) - rm -f $(HTML:.html=.content) - -.PHONY: clean diff --git a/downloads/copilot_tutorial.pdf b/_site/downloads/copilot_tutorial.pdf similarity index 100% rename from downloads/copilot_tutorial.pdf rename to _site/downloads/copilot_tutorial.pdf diff --git a/haskell.css b/_site/haskell.css similarity index 100% rename from haskell.css rename to _site/haskell.css diff --git a/home.css b/_site/home.css similarity index 100% rename from home.css rename to _site/home.css diff --git a/style.css b/_site/style.css similarity index 100% rename from style.css rename to _site/style.css diff --git a/compile.sh b/compile.sh new file mode 100755 index 0000000..26eee40 --- /dev/null +++ b/compile.sh @@ -0,0 +1,9 @@ +#!/bin/bash + +TITLE="$1" +NAV="$(cat nav)" +CONTENT="$(pandoc $2 -t html)" +TARGET="_site/$(basename $2 .md).html" +TEMPLATE="$3" +mkdir -p _site/ +env TITLE="$TITLE" NAV="$NAV" CONTENT="$CONTENT" envsubst '${TITLE}':'${NAV}':'${CONTENT}' < tpl/$TEMPLATE > $TARGET diff --git a/contact.md b/contact.md index 82b25e9..952f576 100644 --- a/contact.md +++ b/contact.md @@ -9,8 +9,8 @@ and discuss the issue. ## General Questions For general questions about Copilot, questions that are unsuited to be posted publicly or if you are not in the possession of a GitHub account, please send -your questions to the maintainer, Frank Dedden -[dev@dedden.net](mailto://dev@dedden.net). +your questions to the maintainer, Ivan Perez +[ivan.perezdominguez@nasa.gov](mailto://ivan.perezdominguez@nasa.gov). ## Previous developers diff --git a/documentation.md b/documentation.md index 3c6089e..5610fd6 100644 --- a/documentation.md +++ b/documentation.md @@ -3,7 +3,7 @@ A manual to Copilot can be downloaded [here](downloads/copilot_tutorial.pdf). Copilot comes with a set of examples as part of its distribution, available in the [Examples -directory](https://github.com/Copilot-Language/Copilot/tree/master/Examples) of +directory](https://github.com/Copilot-Language/Copilot/tree/master/copilot/examples) of the repository. @@ -22,6 +22,9 @@ that make up Copilot, that all share a single repository: new back-end to Copilot. ([Hackage](https://hackage.haskell.org/package/copilot-core)) +- `copilot-interpreter`: A backend for simulating Copilot specifications. + ([Hackage](https://hackage.haskell.org/package/copilot-interpreter)) + - `copilot-language`: The front-end of Copilot defining the user language. A user of Copilot typically interacts with this library. ([Hackage](https://hackage.haskell.org/package/copilot-language)) diff --git a/download.md b/download.md index f0d845c..4620e7b 100644 --- a/download.md +++ b/download.md @@ -1,7 +1,7 @@ # Download & Installing Copilot is implemented as a Embedded Domain Specific Language in Haskell. -Currently Copilot 3.1 requires a version of the Glasgow Haskell Compiler (GHC) -of at least 8.0 to be installed. The recommended way to do this is by +Currently Copilot 3.14 requires a version of the Glasgow Haskell Compiler (GHC) +of at least 8.6 to be installed. The recommended way to do this is by installing the [Haskell Platform](https://www.haskell.org/platform/). The Haskell platform comes with the compiler and basic tools necessary to install Copilot. diff --git a/home.md b/home.md index a684674..b929cab 100644 --- a/home.md +++ b/home.md @@ -1,32 +1,59 @@ ## News -**Release 3.5 -- 2021-09-07** +**Release 4.7.1 -- 2026-05-07** -We are pleased to announce the release of Copilot 3.5, a stream-based DSL for +We are pleased to announce the release of Copilot 4.7.1, a stream-based DSL for writing and monitoring embedded C programs, with an emphasis on correctness and hard realtime requirements. Copilot is typically used as a high-level runtime verification framework, and supports temporal logic (LTL, PTLTL and MTL), clocks and voting algorithms. -Among others, Copilot has been used at the Safety Critical Avionics Systems +Among others, Copilot is being used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This new release introduces a simple but important feature to make Copilot code -more modular: the name of Copilot's main entry point in the generated C code, -known as the step function, can now be customized. This will allow -specifications to be defined in different modules, compiled separately, and -linked as part of the same C executable. It will also facilitate interoperation -with other systems that consider 'step' a reserved a global name. -Additionally, this release introduces other fixes in the code and in the -documentation, and deprecates definitions that have been superseded. +This release introduces several improvements to Copilot: -Current emphasis is on facilitating the use with other systems, and improving -the codebase in terms of stability and test coverage. Users are encouraged to -participate by opening issues and asking questions via our [github -repo](https://github.com/copilot-language/copilot). +- Fix corner cases in the treatment of special floating point numbers in the + Bluespec backend and `copilot-theorem`. +- Fix errors in examples in `copilot-theorem` that use Z3. -## Licence -Copilot is distributed under the BSD-3-Clause licence, which can be found +- Add to `copilot-libraries` a module to perform sanity checks of Copilot + specifications. + +- Add to `copilot-libraries` a module to facilitate implementing state + machines. + +We expect those new modules to grow in the future. + +The new implementation is compatible with versions of GHC from 8.6 to 9.10, as +well as with Stackage Nightly. + +This release has been made possible thanks to key submissions from Ryan Scott +(Galois), and Chris Hathhorn (Galois). We are grateful to them for their timely +contributions, and for making Copilot better every day. + +Details are available +[here](https://github.com/Copilot-Language/copilot/milestone/38?closed=1), +and +[here](https://github.com/Copilot-Language/copilot/releases/tag/v4.7.1). + +As always, we're releasing exactly 2 months since the last release. Our next +release is scheduled for Jul 7th, 2026. + +We want to remind the community that Copilot is now accepting code +contributions from external participants again. Please see the discussions and +the issues to learn how to participate. + +Current emphasis is on improving the codebase in terms of performance, +stability and test coverage, removing unnecessary dependencies, hiding internal +definitions, formatting the code to meet our new coding standards, and +simplifying the Copilot interface. Users are encouraged to participate by +opening issues, asking questions, extending the implementation, and sending bug +fixes via our [github repo](https://github.com/copilot-language/copilot). + +## License + +Copilot is distributed under the BSD-3-Clause license, which can be found [here](https://raw.githubusercontent.com/Copilot-Language/Copilot/master/LICENSE). ## Acknowledgements diff --git a/map b/map deleted file mode 100644 index 98546b5..0000000 --- a/map +++ /dev/null @@ -1,6 +0,0 @@ -T home.html Home -T about.html About -T download.html Download -T documentation.html Documentation -T contact.html Contact -L https://github.com/copilot-language/copilot Source Code diff --git a/nav b/nav new file mode 100644 index 0000000..e12e9b5 --- /dev/null +++ b/nav @@ -0,0 +1,8 @@ +

+Home +About +Download +Documentation +Contact +Source Code +

diff --git a/tpl/default b/tpl/default old mode 100755 new mode 100644 index e9cad31..e82b92c --- a/tpl/default +++ b/tpl/default @@ -1,24 +1,20 @@ -#!/bin/sh - -cat < - - Copilot: $TITLE - - - - -
- - -
- $CONTENT -
-
- + + Copilot: $TITLE + + + + +
+ + +
+ $CONTENT +
+
+ -! diff --git a/tpl/home b/tpl/home index fadb881..c50ead7 100644 --- a/tpl/home +++ b/tpl/home @@ -1,40 +1,39 @@ -#!/bin/sh - -cat < - - Copilot: $TITLE - - - - - -
- - -
-
-

- Copilot is a realtime programming language and Runtime Verification - framework. It allows users to write concise programs in a simple - but powerful way using a stream-based approach. -

-

- Programs can be interpreted for testing, or translated C99 code to be - incorporated in a project, or as a standalone application. The C99 - backend ensures us that the output is constant in memory and time, - making it suitable for systems with hard realtime requirements. -

-

- Learn more about the project... -

-
-
- 
-- Raw temperature from sensor, range -50.0C to 100.0C.
+    
+        Copilot: $TITLE
+        
+        
+        
+        
+    
+        

+            
+            
+            

+                

+                    

+                        Copilot is a realtime programming language and Runtime Verification
+                        framework.  It allows users to write concise programs in a simple
+                        but powerful way using a stream-based approach.
+                    

+                    

+                        Programs can be interpreted for testing, or translated C99 code to be
+                        incorporated in a project, or as a standalone application. The C99
+                        backend ensures us that the output is constant in memory and time,
+                        making it suitable for systems with hard realtime requirements.
+                    

+                    

+                        Learn more about the project...
+                    

+                

+                

+                    
-- Raw temperature from sensor, range -50.0C to 100.0C.
 temp :: Stream Word8
 temp = extern "temperature" Nothing
 
@@ -46,12 +45,11 @@ ctemp = (unsafeCast temp) * (150.0 / "heaton"  (ctemp < 18.0) [arg ctemp]
   trigger "heatoff" (ctemp > 21.0) [arg ctemp]

-				

-			

-			

-				$CONTENT
-			

-		

-	
+
+
+
+ $CONTENT +
+
+ -!