<commit_before>#!/bin/bash

# Script to run fsdoc on certain dirs in the FStar repo.
# Currently, gets called by the VSTF "FStar, Docs, Linux, CI" Build Defn. 
# The $PAT value is stored in that Build Defn.  
set -x # debug on

echo Running fsdoc in `pwd`

# SI: we assume F* has been built and we are in it. 

# make the output dir
FSDOC_ODIR=fsdoc_odir
mkdir -p "$FSDOC_ODIR"

# fsdoc ulib/*.fst* 
pushd ulib
# Get fst, fsti files (files are sorted by default). 
FST_FILES=(*.fst *.fsti)
../bin/fstar-any.sh --odir "../$FSDOC_ODIR" --doc ${FST_FILES[*]} 
popd

# pandoc : md -> html
## FST_FILES
pushd $FSDOC_ODIR 
for f in "${FST_FILES[@]}"
do
    fe=`basename $f` # SI: should just be able to strip -s md if fsdoc outputs X.fst.md. 
    f="${fe%.*}"     #
    md="${f}.md"
    html="${f}.html"
    pandoc $md -f markdown -t html -o $html
done
## index.md 
pandoc index.md -f markdown -t html -o index.html
popd

# push fstarlang.github.io with latest html
mkdir fstarlang.github.io
pushd fstarlang.github.io
git init
git config user.name "fsdocbuild"
git config user.email "<EMAIL>"
git pull https://$PAT@github.com/FStarLang/fstarlang.github.io<commit_msg>Comments.<commit_after>#!/bin/bash

# Script to run fsdoc on certain dirs in the FStar repo.
# Currently, this script gets called by the VSTF "FStar, Docs, Linux, CI"
# Build Defn. The $PAT env var is stored in that Build Defn.  
set -x # debug on

echo Running fsdoc in `pwd`

# SI: we assume F* has been built and we are in it. 

# make the output dir
FSDOC_ODIR=fsdoc_odir
mkdir -p "$FSDOC_ODIR"

# fsdoc the output dir.  
pushd ulib
# Get fst, fsti files (files are name-sorted by default). 
FST_FILES=(*.fst *.fsti)
../bin/fstar-any.sh --odir "../$FSDOC_ODIR" --doc ${FST_FILES[*]} 
popd

# pandoc : md -> html
## FST_FILES
pushd $FSDOC_ODIR 
for f in "${FST_FILES[@]}"
do
    fe=`basename $f` # SI: should just be able to strip -s md if fsdoc outputs X.fst.md. 
    f="${fe%.*}"     #
    md="${f}.md"
    html="${f}.html"
    pandoc $md -f markdown -t html -o $html
done
## index.md 
pandoc index.md -f markdown -t html -o index.html
popd

# push fstarlang.github.io with latest html.
# The flow is described at https://github.com/blog/1270-easier-builds-and-deployments-using-git-over-https-and-oauth;
# $PAT is stored in the Build Defn. 
mkdir fstarlang.github.io
pushd fstarlang.github.io
git init
git config user.name "fsdocbuild"
git config user.email "<EMAIL>"
git pull https://$PAT@github.com/FStarLang/fstarlang.github.io
{'fraction_non_alphanumeric': 0.13656387665198239, 'fraction_numerical': 0.0016019223067681217, 'mean_word_length': 3.35191637630662, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 7, 'https://': 3, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 2, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6028343', 'n_tokens_mistral': 1007, 'n_tokens_neox': 966, 'n_words': 323}