Erik Martin-Dorel erikmd

References on OCaml

the official OCaml documentation — in particular, start with:
the so-called 99 problems in OCaml (a collection of quite standard exercises);
the Real World OCaml (an online book providing a comprehensive insight on OCaml);
the official OCaml reference manual;
it might also be useful to have by hand the URL of the doc of the Stdlib module (i.e., the module of the standard library that is always loaded by default);

A "shall" or "shall not" requirement that appears outside of a constraint is violated (clause 4).
A nonempty source file does not end in a new-line character which is not immediately preceded by a backslash character or ends in a partial preprocessing token or comment (5.1.1.2).
Token concatenation produces a character sequence matching the syntax of a universal character name (5.1.1.2).
A program in a hosted environment does not define a function named main using one of the specified forms (5.1.2.2.1).
A character not in the basic source character set is encountered in a source file, except in an identifier, a character constant, a string literal, a header name, a comment, or a preprocessing token that is never converted to a token (5.2.1).
An identifier, comment, string literal, character constant, or header name contains an invalid multibyte character or does not

In order to deploy using SSH, we need a SSH keypair. Please use an algorithm strong enough and also supported by GHA and your remote host.

You can use the command below to generate a keypair:

ssh-keygen -t ed25519 -C gha@vm-YourLogin -f ~/.ssh/id_gha

For this use case, don't use a passphrase (just type Return to select an empty passphrase).

	# This file was generated from `meta.yml`, please do not edit manually.
	# Follow the instructions on https://github.com/coq-community/templates to regenerate.
	name: Docker CI

	on:
	push:
	branches:
	- main
	- ITP2023
	pull_request:

	#!/bin/bash

	usage="
	Usage:
	wall [options] [message]

	Write a message to all users.

	Options:
	-n, --nobanner do not print banner

	[0KRunning with gitlab-runner 15.6.0~beta.186.ga889181a (a889181a)[0;m
	[0K on blue-2.shared.runners-manager.gitlab.com/default XxUrkriX[0;m
	section_start:1668295707:prepare_executor
	[0K[0K[36;1mPreparing the "docker+machine" executor[0;m[0;m
	[0KUsing Docker executor with image docker:latest ...[0;m
	[0KStarting service docker:dind ...[0;m
	[0KPulling docker image docker:dind ...[0;m
	[0KUsing docker image sha256:5daac9489dc300a47bcb0ea96855ff17e5353aaab9065dbe19b890f480626683 for docker:dind with digest docker@sha256:659bd125658c3f2a28d1a51418853cf85c439df863e3eff0dcc3a0c30feadbb6 ...[0;m
	[0KWaiting for services to be up and running (timeout 30 seconds)...[0;m
	[0KPulling docker image docker:latest ...[0;m

	[0KRunning with gitlab-runner 15.6.0~beta.186.ga889181a (a889181a)[0;m
	[0K on blue-3.shared.runners-manager.gitlab.com/default zxwgkjAP[0;m
	section_start:1668296743:prepare_executor
	[0K[0K[36;1mPreparing the "docker+machine" executor[0;m[0;m
	[0KUsing Docker executor with image docker:latest ...[0;m
	[0KStarting service docker:dind ...[0;m
	[0KPulling docker image docker:dind ...[0;m
	[0KUsing docker image sha256:5daac9489dc300a47bcb0ea96855ff17e5353aaab9065dbe19b890f480626683 for docker:dind with digest docker@sha256:659bd125658c3f2a28d1a51418853cf85c439df863e3eff0dcc3a0c30feadbb6 ...[0;m
	[0KWaiting for services to be up and running (timeout 30 seconds)...[0;m
	[0KPulling docker image docker:latest ...[0;m

	#!/usr/bin/env python3
	"""
	License: MIT License
	Copyright (c) 2023 Miel Donkers

	Very simple HTTP server in python for logging requests
	Usage::
	./server.py [<port>]
	"""
	from http.server import BaseHTTPRequestHandler, HTTPServer

	(* Rappel syntaxe Coq : les commentaires s'écrivent entre (* et ). )

	(******************************)
	(* Tutoriel (Cours/TP) de Coq *)
	(******************************)

	(* Voir aussi ces supports de Cours (UE ILU3, L3 Info, UPS) :

	https://pfitaxel.github.io/ilu3-coq-alectryon/