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