Printf not working with float data type

I’m trying to print a float using printf, but it just appears as a blank space. I’ve had no problems printing string or int data types.

#include "mbed-drivers/mbed.h"

static void blinky(void) {
    static Serial pc(PTC17,PTC16);
    static DigitalOut led(LED1);
    led = !led;
    float x = 1.2345;
    int y = 5;

    pc.printf("%f \r\n", x);
    pc.printf("%i \r\n", y);

void app_start(int, char**) {

When compiling with gcc, floating point isn’t currently supported in printf as it significantly increases code size (even if you’re not using floating point).

We intend to introduce a configuration option to make it possible to enable floating point printing in the future though.

Please could you open an issue for this on our base gcc target description, at, so that we can plan the work to address this!

Ok. Is there a way that I can convert it to a string for debugging purposes?

If you only need an approximate value the converting it to an integer (possibly with scaling) is the easiest option. e.g.

pc.printf("x*100 ~= %i \r\n", int(x*100));