<commit_before>#!/bin/bash
set -e
set -x

git_org=tahina-pro
git_remote=tahina-pro

# Check if the user has provided a GitHub authentication token
[[ -n $SATS_TOKEN ]]

# Detect the F* directory and enter it
fstar_home=$(cd `dirname $0`/.. && pwd)
pushd "$fstar_home"

# Fail if the state is dirty
git diff --staged --exit-code
git diff --exit-code

# Detect the F* version number
if [[ -n $FSTAR_VERSION ]] ; then
    # It is provided by the user
    my_tag="$FSTAR_VERSION"
elif my_tag=$(git describe --exact-match) ; then
    # It is the tag of the current commit
    # Check that there is only one tag
    [[ $(echo $my_tag | wc -w) -eq 1 ]]
else
    # Generate a new tag under the vYYYY.MM.DD format
    my_tag=$(date '+v%Y.%m.%d')
fi

# Check if the commit pointed to by that tag (if any) points to the current commit
this_commit=$(git rev-parse HEAD)
git_push_tag_cmd=true
if tagged_commit=$(git show-ref --tags --hash $my_tag) ; then
    [[ $tagged_commit = $this_commit ]]
else
    # the tag does not exist, so we can apply it
    # and we will need to push it before pushing the release
    git_push_tag_cmd="git push $git_remote $my_tag"
    git tag "$my_tag"
fi

# Overwrite the version number. We need to strip the initial v. Note:
# this version number will not be committed, because, if a user
# compiles from master, then they should have a dev version number,
# but the version number used at compilation time will be read from
# version.txt
my_version=$(echo $my_tag | sed 's!^v!!')
echo $my_version > version.txt<commit_msg>what if the tag is a branch<commit_after>#!/bin/bash
set -e
set -x

git_org=tahina-pro
git_remote=tahina-pro

# Check if the user has provided a GitHub authentication token
[[ -n $SATS_TOKEN ]]

# Detect the F* directory and enter it
fstar_home=$(cd `dirname $0`/.. && pwd)
pushd "$fstar_home"

# Fail if the state is dirty
git diff --staged --exit-code
git diff --exit-code

# Detect the F* version number
if [[ -n $FSTAR_VERSION ]] ; then
    # It is provided by the user
    my_tag="$FSTAR_VERSION"
elif my_tag=$(git describe --exact-match) ; then
    # It is the tag of the current commit
    # Check that there is only one tag
    [[ $(echo $my_tag | wc -w) -eq 1 ]]
else
    # Generate a new tag under the vYYYY.MM.DD format
    my_tag=$(date '+v%Y.%m.%d')
fi

# Check if the commit pointed to by that tag (if any) points to the current commit
this_commit=$(git rev-parse HEAD)
git_push_tag_cmd=true
if tagged_commit=$(git show-ref --tags --hash $my_tag) && [[ -n $tagged_commit ]] ; then
    [[ $tagged_commit = $this_commit ]]
else
    # the tag does not exist, but check that it does not correspond to
    # an existing branch
    ! git rev-parse "$my_tag"
    # so we can apply it
    # and we will need to push it before pushing the release
    git_push_tag_cmd="git push $git_remote $my_tag"
    git tag "$my_tag"
fi

# Overwrite the version number. We need to strip the initial v. Note:
# this version number will not be committed, because, if a user
# compiles from master, then they should have a dev version number,
# but the version number used at compilation time will be read from
# version.txt
my_version=$(echo $my_tag | sed 's!^v!!')
echo $my_version > version.txt
{'fraction_non_alphanumeric': 0.10498606379684113, 'fraction_numerical': 0.0012387736141220192, 'mean_word_length': 3.5174825174825175, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, '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': '1747449', 'n_tokens_mistral': 1081, 'n_tokens_neox': 1051, 'n_words': 445}