1#!/usr/bin/env perl 2# 3# Copyright 2020, Data61 4# Commonwealth Scientific and Industrial Research Organisation (CSIRO) 5# ABN 41 687 119 230. 6# 7# This software may be distributed and modified according to the terms 8# of the GNU General Public License version 2. Note that NO WARRANTY is 9# provided. See "LICENSE_GPLv2.txt" for details. 10# 11# @TAG(DATA61_GPL) 12# 13 14use strict; 15use warnings; 16 17use File::Path qw(make_path); 18use File::Which qw(which); 19use IO::Handle; 20use Time::Piece; 21 22die "usage: $0 <output-dir> <cogent-binary>\n" 23 unless scalar @ARGV == 2; 24 25my $output_dir = shift; 26my $cogent_bin = shift; 27my $filename = 'cogent.1'; 28my $output_file = $output_dir . '/' . $filename; 29 30make_path $output_dir unless (-d $output_dir); 31 32open my $out, '>', $output_file 33 or die "can't write to $output_file: $!"; 34 35system "which $cogent_bin >/dev/null"; 36die "couldn't find Cogent executable" unless defined $?; 37 38my $version = `$cogent_bin -v`; 39$version =~ /: (.*)/; 40$version = $1; 41 42my $date = localtime->strftime('%B %d, %Y'); 43 44$out->print(<<__EOF__ =~ s/\n\n/\n/gmr); 45.\\" 46.\\" Manual page for Cogent. 47.\\" 48.\\" 49.\\" Copyright 2020, Data61 50.\\" Commonwealth Scientific and Industrial Research Organisation (CSIRO) 51.\\" ABN 41 687 119 230. 52.\\" 53.\\" This software may be distributed and modified according to the terms 54.\\" of the GNU General Public License version 2. Note that NO WARRANTY is 55.\\" provided. See "LICENSE_GPLv2.txt" for details. 56.\\" 57.\\" \@TAG(DATA61_GPL) 58.\\" 59 60.Dd $date 61.Dt COGENT 1 62.Os Data61 63 64.Sh NAME 65.Nm cogent 66.Nd a compiler for building high-assurance file-systems 67 68.Sh SYNOPSIS 69.Nm 70.Ar COMMAND... 71.Bq Ar FLAG... 72.Ar FILENAME 73 74.Sh DESCRIPTION 75The 76.Nm 77compiler takes a set of commands, 78with a list of optional flags, 79and an input file. 80It is used to compile Cogent source code 81and generate C code, 82plus Isabelle/HOL specifications and proofs 83to show that the generated C code 84has the same semantics as the source program 85(and its shallow HOL embedding). 86The 87.Nm 88compiler supports FFI to interact with existing C code. 89The user needs to write a thin wrapper in C, 90with antiquoted Cogent identifiers, 91in order to access Cogent functions and datatypes. 92 93__EOF__ 94 95open my $fh, "$cogent_bin -h4 |" 96 or die "couldn't run '$cogent_bin': $!"; 97while (<$fh>) { 98 chomp; 99 100 # Drop the blank line. 101 next if $_ eq ''; 102 103 # Transform headers. 104 $out->print(".Sh $1\n") and next 105 if /\A(COMMANDS|FLAGS):\Z/; 106 107 # TODO(jashank): munge options into mandoc format 108 $out->print("$_\n"); 109} 110$fh->close; 111 112$out->print(<<__EOF__ =~ s/\n\n/\n/gmr); 113.\\" .Sh ENVIRONMENT 114.\\" .Sh FILES 115.\\" .Sh EXIT STATUS 116.\\" .Sh EXAMPLES 117.\\" .Sh DIAGNOSTICS 118 119.Sh SEE ALSO 120The full documentation for 121.Nm 122is maintained online. 123.Bl -dash -compact 124.It 125.Lk https://cogent.readthedocs.io/ 126.It 127.Lk https://ts.data61.csiro.au/projects/TS/cogent.pml 128.It 129.Lk https://github.com/NICTA/cogent 130.El 131 132.\\" .Sh STANDARDS 133 134.\\" .Sh HISTORY 135 136.Sh AUTHORS 137.An Trustworthy Systems at Data61, CSIRO 138 139.\\" .Sh CAVEATS 140 141.\\" .Sh BUGS 142 143__EOF__ 144 145$out->close; 146